mathlib documentation

data.set.finite

Finite sets #

This file defines predicates finite : set α → Prop and infinite : set α → Prop and proves some basic facts about finite sets.

inductive set.finite {α : Type u} (s : set α) :
Prop

A set is finite if the subtype is a fintype, i.e. there is a list that enumerates its members.

theorem set.finite_def {α : Type u} {s : set α} :
def set.infinite {α : Type u} (s : set α) :
Prop

A set is infinite if it is not finite.

Equations
noncomputable def set.finite.fintype {α : Type u} {s : set α} (h : s.finite) :

The subtype corresponding to a finite set is a finite type. Note that because finite isn't a typeclass, this will not fire if it is made into an instance

Equations
noncomputable def set.finite.to_finset {α : Type u} {s : set α} (h : s.finite) :

Get a finset from a finite set

Equations
@[simp]
theorem set.not_infinite {α : Type u} {s : set α} :
@[simp]
theorem set.finite.mem_to_finset {α : Type u} {s : set α} (h : s.finite) {a : α} :
@[simp]
theorem set.finite.to_finset.nonempty {α : Type u} {s : set α} (h : s.finite) :
@[simp]
theorem set.finite.coe_to_finset {α : Type u} {s : set α} (h : s.finite) :
@[simp]
theorem set.finite.coe_sort_to_finset {α : Type u} {s : set α} (h : s.finite) :
@[simp]
theorem set.finite_empty_to_finset {α : Type u} (h : .finite) :
@[simp]
theorem set.finite.to_finset_inj {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
theorem set.subset_to_finset_iff {α : Type u} {s : finset α} {t : set α} (ht : t.finite) :
@[simp]
theorem set.finite_to_finset_eq_empty_iff {α : Type u} {s : set α} {h : s.finite} :
theorem set.finite.exists_finset {α : Type u} {s : set α} :
s.finite(∃ (s' : finset α), ∀ (a : α), a s' a s)
theorem set.finite.exists_finset_coe {α : Type u} {s : set α} (hs : s.finite) :
∃ (s' : finset α), s' = s
@[protected, instance]
def set.finset.can_lift {α : Type u} :
can_lift (set α) (finset α)

Finite sets can be lifted to finsets.

Equations
theorem set.finite_mem_finset {α : Type u} (s : finset α) :
{a : α | a s}.finite
theorem set.finite.of_fintype {α : Type u} [fintype α] (s : set α) :
theorem set.exists_finite_iff_finset {α : Type u} {p : set α → Prop} :
(∃ (s : set α), s.finite p s) ∃ (s : finset α), p s
theorem set.finite.fin_embedding {α : Type u} {s : set α} (h : s.finite) :
∃ (n : ) (f : fin n α), set.range f = s
theorem set.finite.fin_param {α : Type u} {s : set α} (h : s.finite) :
∃ (n : ) (f : fin n → α), function.injective f set.range f = s
def set.decidable_mem_of_fintype {α : Type u} [decidable_eq α] (s : set α) [fintype s] (a : α) :

Membership of a subset of a finite type is decidable.

Using this as an instance leads to potential loops with subtype.fintype under certain decidability assumptions, so it should only be declared a local instance.

Equations
@[protected, instance]
def set.fintype_empty {α : Type u} :
Equations
theorem set.empty_card {α : Type u} :
@[simp]
theorem set.empty_card' {α : Type u} {h : fintype } :
@[simp]
theorem set.finite_empty {α : Type u} :
@[protected, instance]
def set.finite.inhabited {α : Type u} :
inhabited {s // s.finite}
Equations
def set.fintype_insert' {α : Type u} {a : α} (s : set α) [fintype s] (h : a s) :

A fintype structure on insert a s.

Equations
theorem set.card_fintype_insert' {α : Type u} {a : α} (s : set α) [fintype s] (h : a s) :
@[simp]
theorem set.card_insert {α : Type u} {a : α} (s : set α) [fintype s] (h : a s) {d : fintype (insert a s)} :
theorem set.card_image_of_inj_on {α : Type u} {β : Type v} {s : set α} [fintype s] {f : α → β} [fintype (f '' s)] (H : ∀ (x : α), x s∀ (y : α), y sf x = f yx = y) :
theorem set.card_image_of_injective {α : Type u} {β : Type v} (s : set α) [fintype s] {f : α → β} [fintype (f '' s)] (H : function.injective f) :
@[protected, instance]
def set.fintype_insert {α : Type u} [decidable_eq α] (a : α) (s : set α) [fintype s] :
Equations
@[simp]
theorem set.finite.insert {α : Type u} (a : α) {s : set α} :
s.finite(insert a s).finite
theorem set.to_finset_insert {α : Type u} [decidable_eq α] {a : α} {s : set α} (hs : s.finite) :
@[simp]
theorem set.insert_to_finset {α : Type u} [decidable_eq α] {a : α} {s : set α} [fintype s] :
theorem set.finite.induction_on {α : Type u} {C : set α → Prop} {s : set α} (h : s.finite) (H0 : C ) (H1 : ∀ {a : α} {s : set α}, a ss.finiteC sC (insert a s)) :
C s
theorem set.finite.dinduction_on {α : Type u} {C : Π (s : set α), s.finite → Prop} {s : set α} (h : s.finite) (H0 : C set.finite_empty) (H1 : ∀ {a : α} {s : set α}, a s∀ (h : s.finite), C s hC (insert a s) _) :
C s h
@[protected, instance]
def set.fintype_singleton {α : Type u} (a : α) :
Equations
@[simp]
theorem set.card_singleton {α : Type u} (a : α) :
@[simp]
theorem set.finite_singleton {α : Type u} (a : α) :
{a}.finite
theorem set.subsingleton.finite {α : Type u} {s : set α} (h : s.subsingleton) :
theorem set.finite_is_top (α : Type u_1) [partial_order α] :
{x : α | is_top x}.finite
theorem set.finite_is_bot (α : Type u_1) [partial_order α] :
{x : α | is_bot x}.finite
@[protected, instance]
def set.fintype_pure {α : Type u} (a : α) :
Equations
theorem set.finite_pure {α : Type u} (a : α) :
@[protected, instance]
def set.fintype_univ {α : Type u} [fintype α] :
Equations
theorem set.finite_univ {α : Type u} [fintype α] :
noncomputable def set.fintype_of_univ_finite {α : Type u} (H : set.univ.finite) :

If (set.univ : set α) is finite then α is a finite type.

Equations
theorem set.infinite_univ {α : Type u} [h : infinite α] :
theorem set.infinite_coe_iff {α : Type u} {s : set α} :
theorem set.infinite.to_subtype {α : Type u} {s : set α} (h : s.infinite) :
noncomputable def set.infinite.nat_embedding {α : Type u} (s : set α) (h : s.infinite) :

Embedding of into an infinite set.

Equations
theorem set.infinite.exists_subset_card_eq {α : Type u} {s : set α} (hs : s.infinite) (n : ) :
∃ (t : finset α), t s t.card = n
theorem set.infinite.nonempty {α : Type u} {s : set α} (h : s.infinite) :
@[protected, instance]
def set.fintype_union {α : Type u} [decidable_eq α] (s t : set α) [fintype s] [fintype t] :
Equations
theorem set.finite.union {α : Type u} {s t : set α} :
s.finitet.finite(s t).finite
theorem set.finite.sup {α : Type u} {s t : set α} :
s.finitet.finite(s t).finite
theorem set.infinite_of_finite_compl {α : Type u} [infinite α] {s : set α} (hs : s.finite) :
theorem set.finite.infinite_compl {α : Type u} [infinite α] {s : set α} (hs : s.finite) :
@[protected, instance]
def set.fintype_sep {α : Type u} (s : set α) (p : α → Prop) [fintype s] [decidable_pred p] :
fintype {a ∈ s | p a}
Equations
@[protected, instance]
def set.fintype_inter {α : Type u} (s t : set α) [fintype s] [decidable_pred (λ (_x : α), _x t)] :
Equations
def set.fintype_subset {α : Type u} (s : set α) {t : set α} [fintype s] [decidable_pred (λ (_x : α), _x t)] (h : t s) :

A fintype structure on a set defines a fintype structure on its subset.

Equations
theorem set.finite.subset {α : Type u} {s : set α} :
s.finite∀ {t : set α}, t s → t.finite
theorem set.finite.union_iff {α : Type u} {s t : set α} :
theorem set.finite.diff {α : Type u} {s t u : set α} (hs : s.finite) (ht : t.finite) (h : u \ t s) :
theorem set.finite.inter_of_left {α : Type u} {s : set α} (h : s.finite) (t : set α) :
(s t).finite
theorem set.finite.inter_of_right {α : Type u} {s : set α} (h : s.finite) (t : set α) :
(t s).finite
theorem set.finite.inf_of_left {α : Type u} {s : set α} (h : s.finite) (t : set α) :
(s t).finite
theorem set.finite.inf_of_right {α : Type u} {s : set α} (h : s.finite) (t : set α) :
(t s).finite
@[protected]
theorem set.infinite.mono {α : Type u} {s t : set α} (h : s t) :
theorem set.infinite.diff {α : Type u} {s t : set α} (hs : s.infinite) (ht : t.finite) :
(s \ t).infinite
@[protected, instance]
def set.fintype_image {α : Type u} {β : Type v} [decidable_eq β] (s : set α) (f : α → β) [fintype s] :
Equations
@[protected, instance]
def set.fintype_range {α : Type u} {ι : Sort w} [decidable_eq α] (f : ι → α) [fintype (plift ι)] :
Equations
theorem set.finite_range {α : Type u} {ι : Sort w} (f : ι → α) [fintype (plift ι)] :
theorem set.finite.image {α : Type u} {β : Type v} {s : set α} (f : α → β) :
s.finite(f '' s).finite
theorem set.infinite_of_infinite_image {α : Type u} {β : Type v} (f : α → β) {s : set α} (hs : (f '' s).infinite) :
theorem set.finite.dependent_image {α : Type u} {β : Type v} {s : set α} (hs : s.finite) (F : Π (i : α), i s → β) :
{y : β | ∃ (x : α) (hx : x s), y = F x hx}.finite
theorem set.finite.of_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} (h : (f ⁻¹' s).finite) (hf : function.surjective f) :
@[protected, instance]
def set.fintype_map {α β : Type u_1} [decidable_eq β] (s : set α) (f : α → β) [fintype s] :
Equations
theorem set.finite.map {α β : Type u_1} {s : set α} (f : α → β) :
s.finite(f <$> s).finite
def set.fintype_of_fintype_image {α : Type u} {β : Type v} (s : set α) {f : α → β} {g : β → option α} (I : function.is_partial_inv f g) [fintype (f '' s)] :

If a function f has a partial inverse and sends a set s to a set with [fintype] instance, then s has a fintype structure as well.

Equations
theorem set.finite_of_finite_image {α : Type u} {β : Type v} {s : set α} {f : α → β} (hi : set.inj_on f s) :
(f '' s).finite → s.finite
theorem set.finite_image_iff {α : Type u} {β : Type v} {s : set α} {f : α → β} (hi : set.inj_on f s) :
theorem set.infinite_image_iff {α : Type u} {β : Type v} {s : set α} {f : α → β} (hi : set.inj_on f s) :
theorem set.infinite_of_inj_on_maps_to {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (hi : set.inj_on f s) (hm : set.maps_to f s t) (hs : s.infinite) :
theorem set.infinite.exists_ne_map_eq_of_maps_to {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (hs : s.infinite) (hf : set.maps_to f s t) (ht : t.finite) :
∃ (x : α) (H : x s) (y : α) (H : y s), x y f x = f y
theorem set.infinite.exists_lt_map_eq_of_maps_to {α : Type u} {β : Type v} [linear_order α] {s : set α} {t : set β} {f : α → β} (hs : s.infinite) (hf : set.maps_to f s t) (ht : t.finite) :
∃ (x : α) (H : x s) (y : α) (H : y s), x < y f x = f y
theorem set.infinite_range_of_injective {α : Type u} {β : Type v} [infinite α] {f : α → β} (hi : function.injective f) :
theorem set.infinite_of_injective_forall_mem {α : Type u} {β : Type v} [infinite α] {s : set β} {f : α → β} (hi : function.injective f) (hf : ∀ (x : α), f x s) :
theorem set.finite.preimage {α : Type u} {β : Type v} {s : set β} {f : α → β} (I : set.inj_on f (f ⁻¹' s)) (h : s.finite) :
theorem set.finite.preimage_embedding {α : Type u} {β : Type v} {s : set β} (f : α β) (h : s.finite) :
theorem set.finite_option {α : Type u} {s : set (option α)} :
s.finite {x : α | some x s}.finite
@[protected, instance]
def set.fintype_Union {α : Type u} {ι : Sort w} [decidable_eq α] [fintype (plift ι)] (f : ι → set α) [Π (i : ι), fintype (f i)] :
fintype (⋃ (i : ι), f i)
Equations
theorem set.finite_Union {α : Type u} {ι : Sort w} [fintype (plift ι)] {f : ι → set α} (H : ∀ (i : ι), (f i).finite) :
(⋃ (i : ι), f i).finite
def set.fintype_bUnion {α : Type u} [decidable_eq α] {ι : Type u_1} {s : set ι} [fintype s] (f : ι → set α) (H : Π (i : ι), i sfintype (f i)) :
fintype (⋃ (i : ι) (H : i s), f i)

A union of sets with fintype structure over a set with fintype structure has a fintype structure.

Equations
@[protected, instance]
def set.fintype_bUnion' {α : Type u} [decidable_eq α] {ι : Type u_1} {s : set ι} [fintype s] (f : ι → set α) [H : Π (i : ι), fintype (f i)] :
fintype (⋃ (i : ι) (H : i s), f i)
Equations
theorem set.finite.sUnion {α : Type u} {s : set (set α)} (h : s.finite) (H : ∀ (t : set α), t s → t.finite) :
theorem set.finite.bUnion {α : Type u_1} {ι : Type u_2} {s : set ι} {f : Π (i : ι), i sset α} :
s.finite(∀ (i : ι) (H : i s), (f i H).finite)(⋃ (i : ι) (H : i s), f i H).finite
@[protected, instance]
def set.fintype_lt_nat (n : ) :
fintype {i : | i < n}
Equations
@[protected, instance]
def set.fintype_le_nat (n : ) :
fintype {i : | i n}
Equations
theorem set.finite_le_nat (n : ) :
{i : | i n}.finite
theorem set.finite_lt_nat (n : ) :
{i : | i < n}.finite
theorem set.infinite.exists_nat_lt {s : set } (hs : s.infinite) (n : ) :
∃ (m : ) (H : m s), n < m
@[protected, instance]
def set.fintype_prod {α : Type u} {β : Type v} (s : set α) (t : set β) [fintype s] [fintype t] :
Equations
theorem set.finite.prod {α : Type u} {β : Type v} {s : set α} {t : set β} :
s.finitet.finite(s.prod t).finite
@[protected, instance]
def set.fintype_image2 {α : Type u} {β : Type v} {γ : Type x} [decidable_eq γ] (f : α → β → γ) (s : set α) (t : set β) [hs : fintype s] [ht : fintype t] :

image2 f s t is finitype if s and t are.

Equations
theorem set.finite.image2 {α : Type u} {β : Type v} {γ : Type x} (f : α → β → γ) {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) :
def set.fintype_bind {α β : Type u_1} [decidable_eq β] (s : set α) [fintype s] (f : α → set β) (H : Π (a : α), a sfintype (f a)) :

If s : set α is a set with fintype instance and f : α → set β is a function such that each f a, a ∈ s, has a fintype structure, then s >>= f has a fintype structure.

Equations
@[protected, instance]
def set.fintype_bind' {α β : Type u_1} [decidable_eq β] (s : set α) [fintype s] (f : α → set β) [H : Π (a : α), fintype (f a)] :
Equations
theorem set.finite.bind {α β : Type u_1} {s : set α} {f : α → set β} (h : s.finite) (hf : ∀ (a : α), a s(f a).finite) :
(s >>= f).finite
@[protected, instance]
def set.fintype_seq {α : Type u} {β : Type v} [decidable_eq β] (f : set (α → β)) (s : set α) [fintype f] [fintype s] :
Equations
@[protected, instance]
def set.fintype_seq' {α β : Type u} [decidable_eq β] (f : set (α → β)) (s : set α) [fintype f] [fintype s] :
Equations
theorem set.finite.seq {α : Type u} {β : Type v} {f : set (α → β)} {s : set α} (hf : f.finite) (hs : s.finite) :
(f.seq s).finite
theorem set.finite.seq' {α β : Type u} {f : set (α → β)} {s : set α} (hf : f.finite) (hs : s.finite) :
(f <*> s).finite
theorem set.finite.finite_subsets {α : Type u} {a : set α} (h : a.finite) :
{b : set α | b a}.finite

There are finitely many subsets of a given finite set

theorem set.exists_min_image {α : Type u} {β : Type v} [linear_order β] (s : set α) (f : α → β) (h1 : s.finite) :
s.nonempty(∃ (a : α) (H : a s), ∀ (b : α), b sf a f b)
theorem set.exists_max_image {α : Type u} {β : Type v} [linear_order β] (s : set α) (f : α → β) (h1 : s.finite) :
s.nonempty(∃ (a : α) (H : a s), ∀ (b : α), b sf b f a)
theorem set.exists_lower_bound_image {α : Type u} {β : Type v} [hα : nonempty α] [linear_order β] (s : set α) (f : α → β) (h : s.finite) :
∃ (a : α), ∀ (b : α), b sf a f b
theorem set.exists_upper_bound_image {α : Type u} {β : Type v} [hα : nonempty α] [linear_order β] (s : set α) (f : α → β) (h : s.finite) :
∃ (a : α), ∀ (b : α), b sf b f a
theorem finset.finite_to_set {α : Type u} (s : finset α) :
@[simp]
theorem finset.coe_bUnion {α : Type u} {β : Type v} [decidable_eq β] {s : finset α} {f : α → finset β} :
(s.bUnion f) = ⋃ (x : α) (H : x s), (f x)
@[simp]
theorem finset.finite_to_set_to_finset {α : Type u_1} (s : finset α) :
theorem set.finite.pi {δ : Type u_1} [fintype δ] {κ : δ → Type u_2} {t : Π (d : δ), set (κ d)} (ht : ∀ (d : δ), (t d).finite) :

Finite product of finite sets is finite

theorem set.union_finset_finite_of_range_finite {α : Type u} {β : Type v} (f : α → finset β) (h : (set.range f).finite) :
(⋃ (a : α), (f a)).finite

A finite union of finsets is finite.

theorem set.finite_subset_Union {α : Type u} {s : set α} (hs : s.finite) {ι : Type u_1} {t : ι → set α} (h : s ⋃ (i : ι), t i) :
∃ (I : set ι), I.finite s ⋃ (i : ι) (H : i I), t i
theorem set.eq_finite_Union_of_finite_subset_Union {α : Type u} {ι : Type u_1} {s : ι → set α} {t : set α} (tfin : t.finite) (h : t ⋃ (i : ι), s i) :
∃ (I : set ι), I.finite ∃ (σ : {i : ι | i I}set α), (∀ (i : {i : ι | i I}), (σ i).finite) (∀ (i : {i : ι | i I}), σ i s i) t = ⋃ (i : {i : ι | i I}), σ i
theorem set.Union_Inter_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [fintype ι] [linear_order ι'] [nonempty ι'] {s : ι → ι' → set α} (hs : ∀ (i : ι), monotone (s i)) :
(⋃ (j : ι'), ⋂ (i : ι), s i j) = ⋂ (i : ι), ⋃ (j : ι'), s i j

An increasing union distributes over finite intersection.

@[protected, instance]
Equations
theorem set.seq_of_forall_finite_exists {γ : Type u_1} {P : γ → set γ → Prop} (h : ∀ (t : set γ), t.finite(∃ (c : γ), P c t)) :
∃ (u : → γ), ∀ (n : ), P (u n) (u '' set.Iio n)

If P is some relation between terms of γ and sets in γ, such that every finite set t : set γ has some c : γ related to it, then there is a recursively defined sequence u in γ so u n is related to the image of {0, 1, ..., n-1} under u.

(We use this later to show sequentially compact sets are totally bounded.)

theorem set.finite_range_ite {α : Type u} {β : Type v} {p : α → Prop} [decidable_pred p] {f g : α → β} (hf : (set.range f).finite) (hg : (set.range g).finite) :
(set.range (λ (x : α), ite (p x) (f x) (g x))).finite
theorem set.finite_range_const {α : Type u} {β : Type v} {c : β} :
(set.range (λ (x : α), c)).finite
theorem set.range_find_greatest_subset {α : Type u} {P : α → → Prop} [Π (x : α), decidable_pred (P x)] {b : } :
set.range (λ (x : α), nat.find_greatest (P x) b) (finset.range (b + 1))
theorem set.finite_range_find_greatest {α : Type u} {P : α → → Prop} [Π (x : α), decidable_pred (P x)] {b : } :
(set.range (λ (x : α), nat.find_greatest (P x) b)).finite
theorem set.card_lt_card {α : Type u} {s t : set α} [fintype s] [fintype t] (h : s t) :
theorem set.card_le_of_subset {α : Type u} {s t : set α} [fintype s] [fintype t] (hsub : s t) :
theorem set.eq_of_subset_of_card_le {α : Type u} {s t : set α} [fintype s] [fintype t] (hsub : s t) (hcard : fintype.card t fintype.card s) :
s = t
theorem set.subset_iff_to_finset_subset {α : Type u} (s t : set α) [fintype s] [fintype t] :
@[simp]
theorem set.finite.to_finset_mono {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
@[simp]
theorem set.finite.to_finset_strict_mono {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
theorem set.card_range_of_injective {α : Type u} {β : Type v} [fintype α] {f : α → β} (hf : function.injective f) [fintype (set.range f)] :
theorem set.finite.exists_maximal_wrt {α : Type u} {β : Type v} [partial_order β] (f : α → β) (s : set α) (h : s.finite) :
s.nonempty(∃ (a : α) (H : a s), ∀ (a' : α), a' sf a f a'f a = f a')
theorem set.finite.card_to_finset {α : Type u} {s : set α} [fintype s] (h : s.finite) :
theorem set.infinite.exists_not_mem_finset {α : Type u} {s : set α} (hs : s.infinite) (f : finset α) :
∃ (a : α) (H : a s), a f
theorem set.to_finset_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : set α) [fintype s] [fintype s] :
theorem set.to_finset_inter {α : Type u_1} [decidable_eq α] (s t : set α) [fintype (s t)] [fintype s] [fintype t] :
theorem set.to_finset_union {α : Type u_1} [decidable_eq α] (s t : set α) [fintype (s t)] [fintype s] [fintype t] :
theorem set.to_finset_ne_eq_erase {α : Type u_1} [decidable_eq α] [fintype α] (a : α) [fintype {x : α | x a}] :
{x : α | x a}.to_finset = finset.univ.erase a
theorem set.card_ne_eq {α : Type u} [fintype α] (a : α) [fintype {x : α | x a}] :
fintype.card {x : α | x a} = fintype.card α - 1
@[protected]
theorem set.finite.bdd_above {α : Type u} [semilattice_sup α] [nonempty α] {s : set α} (hs : s.finite) :

A finite set is bounded above.

theorem set.finite.bdd_above_bUnion {α : Type u} {β : Type v} [semilattice_sup α] [nonempty α] {I : set β} {S : β → set α} (H : I.finite) :
bdd_above (⋃ (i : β) (H : i I), S i) ∀ (i : β), i Ibdd_above (S i)

A finite union of sets which are all bounded above is still bounded above.

@[protected]
theorem set.finite.bdd_below {α : Type u} [semilattice_inf α] [nonempty α] {s : set α} (hs : s.finite) :

A finite set is bounded below.

theorem set.finite.bdd_below_bUnion {α : Type u} {β : Type v} [semilattice_inf α] [nonempty α] {I : set β} {S : β → set α} (H : I.finite) :
bdd_below (⋃ (i : β) (H : i I), S i) ∀ (i : β), i Ibdd_below (S i)

A finite union of sets which are all bounded below is still bounded below.

@[protected]
theorem finset.bdd_above {α : Type u} [semilattice_sup α] [nonempty α] (s : finset α) :

A finset is bounded above.

@[protected]
theorem finset.bdd_below {α : Type u} [semilattice_inf α] [nonempty α] (s : finset α) :

A finset is bounded below.

@[simp]
theorem fintype.card_subtype_compl {α : Type u} [fintype α] {p : α → Prop} [decidable_pred p] :
fintype.card {x // ¬p x} = fintype.card α - fintype.card {x // p x}
theorem fintype.card_compl_eq_card_compl {α : Type u} [fintype α] {p q : α → Prop} [decidable_pred p] [decidable_pred q] (h : fintype.card {x // p x} = fintype.card {x // q x}) :
fintype.card {x // ¬p x} = fintype.card {x // ¬q x}

If two subtypes of a fintype have equal cardinality, so do their complements.

theorem set.finite_of_forall_between_eq_endpoints {α : Type u_1} [linear_order α] (s : set α) (h : ∀ (x : α), x s∀ (y : α), y s∀ (z : α), z sx yy zx = y y = z) :

If a set s does not contain any elements between any pair of elements x, z ∈ s with x ≤ z (i.e if given x, y, z ∈ s such that x ≤ y ≤ z, then y is either x or z), then s is finite.