mathlib3 documentation

data.set.finite

Finite sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines predicates for finite and infinite sets and provides fintype instances for many set constructions. It also proves basic facts about finite sets and gives ways to manipulate set.finite expressions.

Main definitions #

Implementation #

A finite set is defined to be a set whose coercion to a type has a fintype instance. Since set.finite is Prop-valued, this is the mere fact that the fintype instance exists.

There are two components to finiteness constructions. The first is fintype instances for each construction. This gives a way to actually compute a finset that represents the set, and these may be accessed using set.to_finset. This gets the finset in the correct form, since otherwise finset.univ : finset s is a finset for the subtype for s. The second component is "constructors" for set.finite that give proofs that fintype instances exist classically given other set.finite proofs. Unlike the fintype instances, these do not use any decidability instances since they do not compute anything.

Tags #

finite sets

source
@[protected]
inductive set.finite {α : Type u} (s : set α) :
Prop

A set is finite if there is a finset with the same elements. This is represented as there being a fintype instance for the set coerced to a type.

Note: this is a custom inductive type rather than nonempty (fintype s) so that it won't be frozen as a local instance.

Instances for set.finite
source
theorem set.finite_def {α : Type u} {s : set α} :
s.finite ↔ nonempty (fintype ↥s)
source
theorem set.finite.nonempty_fintype {α : Type u} {s : set α} :
s.finite → nonempty (fintype ↥s)

Alias of the forward direction of set.finite_def.

source
theorem set.finite_coe_iff {α : Type u} {s : set α} :
finite ↥s ↔ s.finite
source
theorem set.to_finite {α : Type u} (s : set α) [finite ↥s] :
s.finite

Constructor for set.finite using a finite instance.

source
@[protected]
theorem set.finite.of_finset {α : Type u} {p : set α} (s : finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) :
p.finite

Construct a finite instance for a set from a finset with the same elements.

source
@[protected]
theorem set.finite.to_subtype {α : Type u} {s : set α} (h : s.finite) :
finite ↥s

Projection of set.finite to its finite instance. This is intended to be used with dot notation. See also set.finite.fintype and set.finite.nonempty_fintype.

source
@[protected]
noncomputable def set.finite.fintype {α : Type u} {s : set α} (h : s.finite) :
fintype ↥s

A finite set coerced to a type is a fintype. This is the fintype projection for a set.finite.

Note that because finite isn't a typeclass, this definition will not fire if it is made into an instance

Equations
source
@[protected]
noncomputable def set.finite.to_finset {α : Type u} {s : set α} (h : s.finite) :
finset α

Using choice, get the finset that represents this set.

Equations
source
theorem set.finite.to_finset_eq_to_finset {α : Type u} {s : set α} [fintype ↥s] (h : s.finite) :
h.to_finset = s.to_finset
source
@[simp]
theorem set.to_finite_to_finset {α : Type u} (s : set α) [fintype ↥s] :
_.to_finset = s.to_finset
source
theorem set.finite.exists_finset {α : Type u} {s : set α} (h : s.finite) :
∃ (s' : finset α), ∀ (a : α), a ∈ s' ↔ a ∈ s
source
theorem set.finite.exists_finset_coe {α : Type u} {s : set α} (h : s.finite) :
∃ (s' : finset α), ↑s' = s
source
@[protected, instance]
def set.finite.can_lift {α : Type u} :
can_lift (set α) (finset α) coe set.finite

Finite sets can be lifted to finsets.

Equations
source
@[protected]
def set.infinite {α : Type u} (s : set α) :
Prop

A set is infinite if it is not finite.

This is protected so that it does not conflict with global infinite.

Equations
source
@[simp]
theorem set.not_infinite {α : Type u} {s : set α} :
¬s.infinite ↔ s.finite
source
@[simp]
theorem set.finite.not_infinite {α : Type u} {s : set α} :
s.finite → ¬s.infinite

Alias of the reverse direction of set.not_infinite.

source
@[protected]
theorem set.finite_or_infinite {α : Type u} (s : set α) :
s.finite ∨ s.infinite

See also finite_or_infinite, fintype_or_infinite.

source
@[protected]
theorem set.infinite_or_finite {α : Type u} (s : set α) :
s.infinite ∨ s.finite

Basic properties of set.finite.to_finset #

source
@[protected, simp]
theorem set.finite.mem_to_finset {α : Type u} {s : set α} {a : α} (h : s.finite) :
a ∈ h.to_finset ↔ a ∈ s
source
@[protected, simp]
theorem set.finite.coe_to_finset {α : Type u} {s : set α} (h : s.finite) :
↑(h.to_finset) = s
source
@[protected, simp]
theorem set.finite.to_finset_nonempty {α : Type u} {s : set α} (h : s.finite) :
h.to_finset.nonempty ↔ s.nonempty
source
theorem set.finite.coe_sort_to_finset {α : Type u} {s : set α} (h : s.finite) :
↥(h.to_finset) = ↥s

Note that this is an equality of types not holding definitionally. Use wisely.

source
@[protected, simp]
theorem set.finite.to_finset_inj {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
hs.to_finset = ht.to_finset ↔ s = t
source
@[simp]
theorem set.finite.to_finset_subset {α : Type u} {s : set α} {hs : s.finite} {t : finset α} :
hs.to_finset ⊆ t ↔ s ⊆ ↑t
source
@[simp]
theorem set.finite.to_finset_ssubset {α : Type u} {s : set α} {hs : s.finite} {t : finset α} :
hs.to_finset ⊂ t ↔ s ⊂ ↑t
source
@[simp]
theorem set.finite.subset_to_finset {α : Type u} {t : set α} {ht : t.finite} {s : finset α} :
s ⊆ ht.to_finset ↔ ↑s ⊆ t
source
@[simp]
theorem set.finite.ssubset_to_finset {α : Type u} {t : set α} {ht : t.finite} {s : finset α} :
s ⊂ ht.to_finset ↔ ↑s ⊂ t
source
@[protected]
theorem set.finite.to_finset_subset_to_finset {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
hs.to_finset ⊆ ht.to_finset ↔ s ⊆ t
source
@[protected]
theorem set.finite.to_finset_ssubset_to_finset {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
hs.to_finset ⊂ ht.to_finset ↔ s ⊂ t
source
@[protected]
theorem set.finite.to_finset_mono {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
s ⊆ t → hs.to_finset ⊆ ht.to_finset

Alias of the reverse direction of set.finite.to_finset_subset_to_finset.

source
@[protected]
theorem set.finite.to_finset_strict_mono {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
s ⊂ t → hs.to_finset ⊂ ht.to_finset

Alias of the reverse direction of set.finite.to_finset_ssubset_to_finset.

source
@[protected, simp]
theorem set.finite.to_finset_set_of {α : Type u} [fintype α] (p : α → Prop) [decidable_pred p] (h : {x : α | p x}.finite) :
h.to_finset = finset.filter p finset.univ
source
@[simp]
theorem set.finite.disjoint_to_finset {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
disjoint hs.to_finset ht.to_finset ↔ disjoint s t
source
@[protected]
theorem set.finite.to_finset_inter {α : Type u} {s t : set α} [decidable_eq α] (hs : s.finite) (ht : t.finite) (h : (s ∩ t).finite) :
h.to_finset = hs.to_finset ∩ ht.to_finset
source
@[protected]
theorem set.finite.to_finset_union {α : Type u} {s t : set α} [decidable_eq α] (hs : s.finite) (ht : t.finite) (h : (s ∪ t).finite) :
h.to_finset = hs.to_finset ∪ ht.to_finset
source
@[protected]
theorem set.finite.to_finset_diff {α : Type u} {s t : set α} [decidable_eq α] (hs : s.finite) (ht : t.finite) (h : (s \ t).finite) :
h.to_finset = hs.to_finset \ ht.to_finset
source
@[protected]
theorem set.finite.to_finset_symm_diff {α : Type u} {s t : set α} [decidable_eq α] (hs : s.finite) (ht : t.finite) (h : (s ∆ t).finite) :
h.to_finset = hs.to_finset ∆ ht.to_finset
source
@[protected]
theorem set.finite.to_finset_compl {α : Type u} {s : set α} [decidable_eq α] [fintype α] (hs : s.finite) (h : sᶜ.finite) :
h.to_finset = hs.to_finsetᶜ
source
@[protected, simp]
theorem set.finite.to_finset_empty {α : Type u} (h : ∅.finite) :
h.to_finset = ∅
source
@[protected, simp]
theorem set.finite.to_finset_univ {α : Type u} [fintype α] (h : set.univ.finite) :
h.to_finset = finset.univ
source
@[protected, simp]
theorem set.finite.to_finset_eq_empty {α : Type u} {s : set α} {h : s.finite} :
h.to_finset = ∅ ↔ s = ∅
source
@[protected, simp]
theorem set.finite.to_finset_eq_univ {α : Type u} {s : set α} [fintype α] {h : s.finite} :
h.to_finset = finset.univ ↔ s = set.univ
source
@[protected]
theorem set.finite.to_finset_image {α : Type u} {β : Type v} {s : set α} [decidable_eq β] (f : α → β) (hs : s.finite) (h : (f '' s).finite) :
h.to_finset = finset.image f hs.to_finset
source
@[protected, simp]
theorem set.finite.to_finset_range {α : Type u} {β : Type v} [decidable_eq α] [fintype β] (f : β → α) (h : (set.range f).finite) :
h.to_finset = finset.image f finset.univ

Fintype instances #

Every instance here should have a corresponding set.finite constructor in the next section.

source
@[protected, instance]
def set.fintype_univ {α : Type u} [fintype α] :
fintype ↥set.univ
Equations
source
noncomputable def set.fintype_of_finite_univ {α : Type u} (H : set.univ.finite) :
fintype α

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

Equations
source
@[protected, instance]
def set.fintype_union {α : Type u} [decidable_eq α] (s t : set α) [fintype ↥s] [fintype ↥t] :
fintype ↥(s ∪ t)
Equations
source
@[protected, instance]
def set.fintype_sep {α : Type u} (s : set α) (p : α → Prop) [fintype ↥s] [decidable_pred p] :
fintype ↥{a ∈ s | p a}
Equations
source
@[protected, instance]
def set.fintype_inter {α : Type u} (s t : set α) [decidable_eq α] [fintype ↥s] [fintype ↥t] :
fintype ↥(s ∩ t)
Equations
source
@[protected, instance]
def set.fintype_inter_of_left {α : Type u} (s t : set α) [fintype ↥s] [decidable_pred (λ (_x : α), _x ∈ t)] :
fintype ↥(s ∩ t)

A fintype instance for set intersection where the left set has a fintype instance.

Equations
source
@[protected, instance]
def set.fintype_inter_of_right {α : Type u} (s t : set α) [fintype ↥t] [decidable_pred (λ (_x : α), _x ∈ s)] :
fintype ↥(s ∩ t)

A fintype instance for set intersection where the right set has a fintype instance.

Equations
source
def set.fintype_subset {α : Type u} (s : set α) {t : set α} [fintype ↥s] [decidable_pred (λ (_x : α), _x ∈ t)] (h : t ⊆ s) :
fintype ↥t

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

Equations
source
@[protected, instance]
def set.fintype_diff {α : Type u} [decidable_eq α] (s t : set α) [fintype ↥s] [fintype ↥t] :
fintype ↥(s \ t)
Equations
source
@[protected, instance]
def set.fintype_diff_left {α : Type u} (s t : set α) [fintype ↥s] [decidable_pred (λ (_x : α), _x ∈ t)] :
fintype ↥(s \ t)
Equations
source
@[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
source
@[protected, instance]
def set.fintype_sUnion {α : Type u} [decidable_eq α] {s : set (set α)} [fintype ↥s] [H : Π (t : ↥s), fintype ↥↑t] :
fintype (↥⋃₀ s)
Equations
source
def set.fintype_bUnion {α : Type u} [decidable_eq α] {ι : Type u_1} (s : set ι) [fintype ↥s] (t : ι → set α) (H : Π (i : ι), i ∈ s → fintype ↥(t i)) :
fintype (↥⋃ (x : ι) (H : x ∈ s), t x)

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

Equations
source
@[protected, instance]
def set.fintype_bUnion' {α : Type u} [decidable_eq α] {ι : Type u_1} (s : set ι) [fintype ↥s] (t : ι → set α) [Π (i : ι), fintype ↥(t i)] :
fintype (↥⋃ (x : ι) (H : x ∈ s), t x)
Equations
source
def set.fintype_bind {α β : Type u_1} [decidable_eq β] (s : set α) [fintype ↥s] (f : α → set β) (H : Π (a : α), a ∈ s → fintype ↥(f a)) :
fintype ↥(s >>= f)

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
source
@[protected, instance]
def set.fintype_bind' {α β : Type u_1} [decidable_eq β] (s : set α) [fintype ↥s] (f : α → set β) [H : Π (a : α), fintype ↥(f a)] :
fintype ↥(s >>= f)
Equations
source
@[protected, instance]
def set.fintype_empty {α : Type u} :
fintype ↥∅
Equations
source
@[protected, instance]
def set.fintype_singleton {α : Type u} (a : α) :
fintype ↥{a}
Equations
source
@[protected, instance]
def set.fintype_pure {α : Type u} (a : α) :
fintype ↥(has_pure.pure a)
Equations
source
@[protected, instance]
def set.fintype_insert {α : Type u} (a : α) (s : set α) [decidable_eq α] [fintype ↥s] :
fintype ↥(has_insert.insert a s)

A fintype instance for inserting an element into a set using the corresponding insert function on finset. This requires decidable_eq α. There is also set.fintype_insert' when a ∈ s is decidable.

Equations
source
def set.fintype_insert_of_not_mem {α : Type u} {a : α} (s : set α) [fintype ↥s] (h : a ∉ s) :
fintype ↥(has_insert.insert a s)

A fintype structure on insert a s when inserting a new element.

Equations
source
def set.fintype_insert_of_mem {α : Type u} {a : α} (s : set α) [fintype ↥s] (h : a ∈ s) :
fintype ↥(has_insert.insert a s)

A fintype structure on insert a s when inserting a pre-existing element.

Equations
source
@[protected, instance]
def set.fintype_insert' {α : Type u} (a : α) (s : set α) [decidable (a ∈ s)] [fintype ↥s] :
fintype ↥(has_insert.insert a s)

The set.fintype_insert instance requires decidable equality, but when a ∈ s is decidable for this particular a we can still get a fintype instance by using set.fintype_insert_of_not_mem or set.fintype_insert_of_mem.

This instance pre-dates set.fintype_insert, and it is less efficient. When decidable_mem_of_fintype is made a local instance, then this instance would override set.fintype_insert if not for the fact that its priority has been adjusted. See Note [lower instance priority].

Equations
source
@[protected, instance]
def set.fintype_image {α : Type u} {β : Type v} [decidable_eq β] (s : set α) (f : α → β) [fintype ↥s] :
fintype ↥(f '' s)
Equations
source
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)] :
fintype ↥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
source
@[protected, instance]
def set.fintype_range {α : Type u} {ι : Sort w} [decidable_eq α] (f : ι → α) [fintype (plift ι)] :
fintype ↥(set.range f)
Equations
source
@[protected, instance]
def set.fintype_map {α β : Type u_1} [decidable_eq β] (s : set α) (f : α → β) [fintype ↥s] :
fintype ↥(f <$> s)
Equations
source
@[protected, instance]
def set.fintype_lt_nat (n : ℕ) :
fintype ↥{i : ℕ | i < n}
Equations
source
@[protected, instance]
def set.fintype_le_nat (n : ℕ) :
fintype ↥{i : ℕ | i ≤ n}
Equations
source
def set.nat.fintype_Iio (n : ℕ) :
fintype ↥(set.Iio n)

This is not an instance so that it does not conflict with the one in src/order/locally_finite.

Equations
source
@[protected, instance]
def set.fintype_prod {α : Type u} {β : Type v} (s : set α) (t : set β) [fintype ↥s] [fintype ↥t] :
fintype ↥(s ×ˢ t)
Equations
source
@[protected, instance]
def set.fintype_off_diag {α : Type u} [decidable_eq α] (s : set α) [fintype ↥s] :
fintype ↥(s.off_diag)
Equations
source
@[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] :
fintype ↥(set.image2 f s t)

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

Equations
source
@[protected, instance]
def set.fintype_seq {α : Type u} {β : Type v} [decidable_eq β] (f : set (α → β)) (s : set α) [fintype ↥f] [fintype ↥s] :
fintype ↥(f.seq s)
Equations
source
@[protected, instance]
def set.fintype_seq' {α β : Type u} [decidable_eq β] (f : set (α → β)) (s : set α) [fintype ↥f] [fintype ↥s] :
fintype ↥(f <*> s)
Equations
source
@[protected, instance]
def set.fintype_mem_finset {α : Type u} (s : finset α) :
fintype ↥{a : α | a ∈ s}
Equations
source
theorem equiv.set_finite_iff {α : Type u} {β : Type v} {s : set α} {t : set β} (hst : ↥s ≃ ↥t) :
s.finite ↔ t.finite

Finset #

source
@[simp]
theorem finset.finite_to_set {α : Type u} (s : finset α) :
↑s.finite

Gives a set.finite for the finset coerced to a set. This is a wrapper around set.to_finite.

source
@[simp]
theorem finset.finite_to_set_to_finset {α : Type u} (s : finset α) :
_.to_finset = s
source
@[simp]
theorem multiset.finite_to_set {α : Type u} (s : multiset α) :
{x : α | x ∈ s}.finite
source
@[simp]
theorem multiset.finite_to_set_to_finset {α : Type u} [decidable_eq α] (s : multiset α) :
_.to_finset = s.to_finset
source
@[simp]
theorem list.finite_to_set {α : Type u} (l : list α) :
{x : α | x ∈ l}.finite

Finite instances #

There is seemingly some overlap between the following instances and the fintype instances in data.set.finite. While every fintype instance gives a finite instance, those instances that depend on fintype or decidable instances need an additional finite instance to be able to generally apply.

Some set instances do not appear here since they are consequences of others, for example subtype.finite for subsets of a finite type.

source
@[protected, instance]
def finite.set.finite_union {α : Type u} (s t : set α) [finite ↥s] [finite ↥t] :
finite ↥(s ∪ t)
source
@[protected, instance]
def finite.set.finite_sep {α : Type u} (s : set α) (p : α → Prop) [finite ↥s] :
finite ↥{a ∈ s | p a}
source
@[protected]
theorem finite.set.subset {α : Type u} (s : set α) {t : set α} [finite ↥s] (h : t ⊆ s) :
finite ↥t
source
@[protected, instance]
def finite.set.finite_inter_of_right {α : Type u} (s t : set α) [finite ↥t] :
finite ↥(s ∩ t)
source
@[protected, instance]
def finite.set.finite_inter_of_left {α : Type u} (s t : set α) [finite ↥s] :
finite ↥(s ∩ t)
source
@[protected, instance]
def finite.set.finite_diff {α : Type u} (s t : set α) [finite ↥s] :
finite ↥(s \ t)
source
@[protected, instance]
def finite.set.finite_range {α : Type u} {ι : Sort w} (f : ι → α) [finite ι] :
finite ↥(set.range f)
source
@[protected, instance]
def finite.set.finite_Union {α : Type u} {ι : Sort w} [finite ι] (f : ι → set α) [∀ (i : ι), finite ↥(f i)] :
finite (↥⋃ (i : ι), f i)
source
@[protected, instance]
def finite.set.finite_sUnion {α : Type u} {s : set (set α)} [finite ↥s] [H : ∀ (t : ↥s), finite ↥↑t] :
finite (↥⋃₀ s)
source
theorem finite.set.finite_bUnion {α : Type u} {ι : Type u_1} (s : set ι) [finite ↥s] (t : ι → set α) (H : ∀ (i : ι), i ∈ s → finite ↥(t i)) :
finite (↥⋃ (x : ι) (H : x ∈ s), t x)
source
@[protected, instance]
def finite.set.finite_bUnion' {α : Type u} {ι : Type u_1} (s : set ι) [finite ↥s] (t : ι → set α) [∀ (i : ι), finite ↥(t i)] :
finite (↥⋃ (x : ι) (H : x ∈ s), t x)
source
@[protected, instance]
def finite.set.finite_bUnion'' {α : Type u} {ι : Type u_1} (p : ι → Prop) [h : finite ↥{x : ι | p x}] (t : ι → set α) [∀ (i : ι), finite ↥(t i)] :
finite (↥⋃ (x : ι) (h : p x), t x)

Example: finite (⋃ (i < n), f i) where f : ℕ → set α and [∀ i, finite (f i)] (when given instances from data.nat.interval).

source
@[protected, instance]
def finite.set.finite_Inter {α : Type u} {ι : Sort u_1} [nonempty ι] (t : ι → set α) [∀ (i : ι), finite ↥(t i)] :
finite (↥⋂ (i : ι), t i)
source
@[protected, instance]
def finite.set.finite_insert {α : Type u} (a : α) (s : set α) [finite ↥s] :
finite ↥(has_insert.insert a s)
source
@[protected, instance]
def finite.set.finite_image {α : Type u} {β : Type v} (s : set α) (f : α → β) [finite ↥s] :
finite ↥(f '' s)
source
@[protected, instance]
def finite.set.finite_replacement {α : Type u} {β : Type v} [finite α] (f : α → β) :
finite ↥{_x : β | ∃ (x : α), f x = _x}
source
@[protected, instance]
def finite.set.finite_prod {α : Type u} {β : Type v} (s : set α) (t : set β) [finite ↥s] [finite ↥t] :
finite ↥(s ×ˢ t)
source
@[protected, instance]
def finite.set.finite_image2 {α : Type u} {β : Type v} {γ : Type x} (f : α → β → γ) (s : set α) (t : set β) [finite ↥s] [finite ↥t] :
finite ↥(set.image2 f s t)
source
@[protected, instance]
def finite.set.finite_seq {α : Type u} {β : Type v} (f : set (α → β)) (s : set α) [finite ↥f] [finite ↥s] :
finite ↥(f.seq s)

Constructors for set.finite #

Every constructor here should have a corresponding fintype instance in the previous section (or in the fintype module).

The implementation of these constructors ideally should be no more than set.to_finite, after possibly setting up some fintype and classical decidable instances.

source
theorem set.finite.of_subsingleton {α : Type u} [subsingleton α] (s : set α) :
s.finite
source
theorem set.finite_univ {α : Type u} [finite α] :
set.univ.finite
source
theorem set.finite_univ_iff {α : Type u} :
set.univ.finite ↔ finite α
source
theorem finite.of_finite_univ {α : Type u} :
set.univ.finite → finite α

Alias of the forward direction of set.finite_univ_iff.

source
theorem set.finite.union {α : Type u} {s t : set α} (hs : s.finite) (ht : t.finite) :
(s ∪ t).finite
source
theorem set.finite.finite_of_compl {α : Type u} {s : set α} (hs : s.finite) (hsc : sᶜ.finite) :
finite α
source
theorem set.finite.sup {α : Type u} {s t : set α} :
s.finite → t.finite → (s ⊔ t).finite
source
theorem set.finite.sep {α : Type u} {s : set α} (hs : s.finite) (p : α → Prop) :
{a ∈ s | p a}.finite
source
theorem set.finite.inter_of_left {α : Type u} {s : set α} (hs : s.finite) (t : set α) :
(s ∩ t).finite
source
theorem set.finite.inter_of_right {α : Type u} {s : set α} (hs : s.finite) (t : set α) :
(t ∩ s).finite
source
theorem set.finite.inf_of_left {α : Type u} {s : set α} (h : s.finite) (t : set α) :
(s ⊓ t).finite
source
theorem set.finite.inf_of_right {α : Type u} {s : set α} (h : s.finite) (t : set α) :
(t ⊓ s).finite
source
theorem set.finite.subset {α : Type u} {s : set α} (hs : s.finite) {t : set α} (ht : t ⊆ s) :
t.finite
source
theorem set.finite.diff {α : Type u} {s : set α} (hs : s.finite) (t : set α) :
(s \ t).finite
source
theorem set.finite.of_diff {α : Type u} {s t : set α} (hd : (s \ t).finite) (ht : t.finite) :
s.finite
source
theorem set.finite_Union {α : Type u} {ι : Sort w} [finite ι] {f : ι → set α} (H : ∀ (i : ι), (f i).finite) :
(⋃ (i : ι), f i).finite
source
theorem set.finite.sUnion {α : Type u} {s : set (set α)} (hs : s.finite) (H : ∀ (t : set α), t ∈ s → t.finite) :
(⋃₀ s).finite
source
theorem set.finite.bUnion {α : Type u} {ι : Type u_1} {s : set ι} (hs : s.finite) {t : ι → set α} (ht : ∀ (i : ι), i ∈ s → (t i).finite) :
(⋃ (i : ι) (H : i ∈ s), t i).finite
source
theorem set.finite.bUnion' {α : Type u} {ι : Type u_1} {s : set ι} (hs : s.finite) {t : Π (i : ι), i ∈ s → set α} (ht : ∀ (i : ι) (H : i ∈ s), (t i H).finite) :
(⋃ (i : ι) (H : i ∈ s), t i H).finite

Dependent version of finite.bUnion.

source
theorem set.finite.sInter {α : Type u_1} {s : set (set α)} {t : set α} (ht : t ∈ s) (hf : t.finite) :
(⋂₀ s).finite
source
theorem set.finite.Union {α : Type u} {ι : Type u_1} {s : ι → set α} {t : set ι} (ht : t.finite) (hs : ∀ (i : ι), i ∈ t → (s i).finite) (he : ∀ (i : ι), i ∉ t → s i = ∅) :
(⋃ (i : ι), s i).finite

If sets s i are finite for all i from a finite set t and are empty for i ∉ t, then the union ⋃ i, s i is a finite set.

source
theorem set.finite.bind {α β : Type u_1} {s : set α} {f : α → set β} (h : s.finite) (hf : ∀ (a : α), a ∈ s → (f a).finite) :
(s >>= f).finite
source
@[simp]
theorem set.finite_empty {α : Type u} :
∅.finite
source
@[protected]
theorem set.infinite.nonempty {α : Type u} {s : set α} (h : s.infinite) :
s.nonempty
source
@[simp]
theorem set.finite_singleton {α : Type u} (a : α) :
{a}.finite
source
theorem set.finite_pure {α : Type u} (a : α) :
(has_pure.pure a).finite
source
@[simp]
theorem set.finite.insert {α : Type u} (a : α) {s : set α} (hs : s.finite) :
(has_insert.insert a s).finite
source
theorem set.finite.image {α : Type u} {β : Type v} {s : set α} (f : α → β) (hs : s.finite) :
(f '' s).finite
source
theorem set.finite_range {α : Type u} {ι : Sort w} (f : ι → α) [finite ι] :
(set.range f).finite
source
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
source
theorem set.finite.map {α β : Type u_1} {s : set α} (f : α → β) :
s.finite → set.finite (f <$> s)
source
theorem set.finite.of_finite_image {α : Type u} {β : Type v} {s : set α} {f : α → β} (h : (f '' s).finite) (hi : set.inj_on f s) :
s.finite
source
theorem set.finite_of_finite_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} (h : (f ⁻¹' s).finite) (hs : s ⊆ set.range f) :
s.finite
source
theorem set.finite.of_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} (h : (f ⁻¹' s).finite) (hf : function.surjective f) :
s.finite
source
theorem set.finite.preimage {α : Type u} {β : Type v} {s : set β} {f : α → β} (I : set.inj_on f (f ⁻¹' s)) (h : s.finite) :
(f ⁻¹' s).finite
source
theorem set.finite.preimage_embedding {α : Type u} {β : Type v} {s : set β} (f : α ↪ β) (h : s.finite) :
(⇑f ⁻¹' s).finite
source
theorem set.finite_lt_nat (n : ℕ) :
{i : ℕ | i < n}.finite
source
theorem set.finite_le_nat (n : ℕ) :
{i : ℕ | i ≤ n}.finite
source
@[protected]
theorem set.finite.prod {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) :
(s ×ˢ t).finite
source
theorem set.finite.of_prod_left {α : Type u} {β : Type v} {s : set α} {t : set β} (h : (s ×ˢ t).finite) :
t.nonempty → s.finite
source
theorem set.finite.of_prod_right {α : Type u} {β : Type v} {s : set α} {t : set β} (h : (s ×ˢ t).finite) :
s.nonempty → t.finite
source
@[protected]
theorem set.infinite.prod_left {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : s.infinite) (ht : t.nonempty) :
(s ×ˢ t).infinite
source
@[protected]
theorem set.infinite.prod_right {α : Type u} {β : Type v} {s : set α} {t : set β} (ht : t.infinite) (hs : s.nonempty) :
(s ×ˢ t).infinite
source
@[protected]
theorem set.infinite_prod {α : Type u} {β : Type v} {s : set α} {t : set β} :
(s ×ˢ t).infinite ↔ s.infinite ∧ t.nonempty ∨ t.infinite ∧ s.nonempty
source
theorem set.finite_prod {α : Type u} {β : Type v} {s : set α} {t : set β} :
(s ×ˢ t).finite ↔ (s.finite ∨ t = ∅) ∧ (t.finite ∨ s = ∅)
source
@[protected]
theorem set.finite.off_diag {α : Type u} {s : set α} (hs : s.finite) :
s.off_diag.finite
source
@[protected]
theorem set.finite.image2 {α : Type u} {β : Type v} {γ : Type x} {s : set α} {t : set β} (f : α → β → γ) (hs : s.finite) (ht : t.finite) :
(set.image2 f s t).finite
source
theorem set.finite.seq {α : Type u} {β : Type v} {f : set (α → β)} {s : set α} (hf : f.finite) (hs : s.finite) :
(f.seq s).finite
source
theorem set.finite.seq' {α β : Type u} {f : set (α → β)} {s : set α} (hf : f.finite) (hs : s.finite) :
(f <*> s).finite
source
theorem set.finite_mem_finset {α : Type u} (s : finset α) :
{a : α | a ∈ s}.finite
source
theorem set.subsingleton.finite {α : Type u} {s : set α} (h : s.subsingleton) :
s.finite
source
theorem set.finite_preimage_inl_and_inr {α : Type u} {β : Type v} {s : set (α ⊕ β)} :
(sum.inl ⁻¹' s).finite ∧ (sum.inr ⁻¹' s).finite ↔ s.finite
source
theorem set.exists_finite_iff_finset {α : Type u} {p : set α → Prop} :
(∃ (s : set α), s.finite ∧ p s) ↔ ∃ (s : finset α), p ↑s
source
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

source
theorem set.finite.pi {δ : Type u_1} [finite δ] {κ : δ → Type u_2} {t : Π (d : δ), set (κ d)} (ht : ∀ (d : δ), (t d).finite) :
(set.univ.pi t).finite

Finite product of finite sets is finite

source
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.

source
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
source
theorem set.finite_range_const {α : Type u} {β : Type v} {c : β} :
(set.range (λ (x : α), c)).finite

Properties #

source
@[protected, instance]
def set.finite.inhabited {α : Type u} :
inhabited {s // s.finite}
Equations
source
@[simp]
theorem set.finite_union {α : Type u} {s t : set α} :
(s ∪ t).finite ↔ s.finite ∧ t.finite
source
theorem set.finite_image_iff {α : Type u} {β : Type v} {s : set α} {f : α → β} (hi : set.inj_on f s) :
(f '' s).finite ↔ s.finite
source
theorem set.univ_finite_iff_nonempty_fintype {α : Type u} :
set.univ.finite ↔ nonempty (fintype α)
source
@[simp]
theorem set.finite.to_finset_singleton {α : Type u} {a : α} (ha : {a}.finite := _) :
set.finite.to_finset ha = {a}
source
@[simp]
theorem set.finite.to_finset_insert {α : Type u} [decidable_eq α] {s : set α} {a : α} (hs : (has_insert.insert a s).finite) :
hs.to_finset = has_insert.insert a _.to_finset
source
theorem set.finite.to_finset_insert' {α : Type u} [decidable_eq α] {a : α} {s : set α} (hs : s.finite) :
_.to_finset = has_insert.insert a hs.to_finset
source
theorem set.finite.to_finset_prod {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) :
hs.to_finset ×ˢ ht.to_finset = _.to_finset
source
theorem set.finite.to_finset_off_diag {α : Type u} {s : set α} [decidable_eq α] (hs : s.finite) :
_.to_finset = hs.to_finset.off_diag
source
theorem set.finite.fin_embedding {α : Type u} {s : set α} (h : s.finite) :
∃ (n : ℕ) (f : fin n ↪ α), set.range ⇑f = s
source
theorem set.finite.fin_param {α : Type u} {s : set α} (h : s.finite) :
∃ (n : ℕ) (f : fin n → α), function.injective f ∧ set.range f = s
source
theorem set.finite_option {α : Type u} {s : set (option α)} :
s.finite ↔ {x : α | option.some x ∈ s}.finite
source
theorem set.finite_image_fst_and_snd_iff {α : Type u} {β : Type v} {s : set (α × β)} :
(prod.fst '' s).finite ∧ (prod.snd '' s).finite ↔ s.finite
source
theorem set.forall_finite_image_eval_iff {δ : Type u_1} [finite δ] {κ : δ → Type u_2} {s : set (Π (d : δ), κ d)} :
(∀ (d : δ), (function.eval d '' s).finite) ↔ s.finite
source
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
source
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
source
theorem set.finite.induction_on {α : Type u} {C : set α → Prop} {s : set α} (h : s.finite) (H0 : C ∅) (H1 : ∀ {a : α} {s : set α}, a ∉ s → s.finite → C s → C (has_insert.insert a s)) :
C s
source
theorem set.finite.induction_on' {α : Type u} {C : set α → Prop} {S : set α} (h : S.finite) (H0 : C ∅) (H1 : ∀ {a : α} {s : set α}, a ∈ S → s ⊆ S → a ∉ s → C s → C (has_insert.insert a s)) :
C S

Analogous to finset.induction_on'.

source
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 h → C (has_insert.insert a s) _) :
C s h
source
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.)

Cardinality #

source
theorem set.empty_card {α : Type u} :
fintype.card ↥∅ = 0
source
@[simp]
theorem set.empty_card' {α : Type u} {h : fintype ↥∅} :
fintype.card ↥∅ = 0
source
theorem set.card_fintype_insert_of_not_mem {α : Type u} {a : α} (s : set α) [fintype ↥s] (h : a ∉ s) :
fintype.card ↥(has_insert.insert a s) = fintype.card ↥s + 1
source
@[simp]
theorem set.card_insert {α : Type u} {a : α} (s : set α) [fintype ↥s] (h : a ∉ s) {d : fintype ↥(has_insert.insert a s)} :
fintype.card ↥(has_insert.insert a s) = fintype.card ↥s + 1
source
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 ∈ s → f x = f y → x = y) :
fintype.card ↥(f '' s) = fintype.card ↥s
source
theorem set.card_image_of_injective {α : Type u} {β : Type v} (s : set α) [fintype ↥s] {f : α → β} [fintype ↥(f '' s)] (H : function.injective f) :
fintype.card ↥(f '' s) = fintype.card ↥s
source
@[simp]
theorem set.card_singleton {α : Type u} (a : α) :
fintype.card ↥{a} = 1
source
theorem set.card_lt_card {α : Type u} {s t : set α} [fintype ↥s] [fintype ↥t] (h : s ⊂ t) :
fintype.card ↥s < fintype.card ↥t
source
theorem set.card_le_of_subset {α : Type u} {s t : set α} [fintype ↥s] [fintype ↥t] (hsub : s ⊆ t) :
fintype.card ↥s ≤ fintype.card ↥t
source
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
source
theorem set.card_range_of_injective {α : Type u} {β : Type v} [fintype α] {f : α → β} (hf : function.injective f) [fintype ↥(set.range f)] :
fintype.card ↥(set.range f) = fintype.card α
source
theorem set.finite.card_to_finset {α : Type u} {s : set α} [fintype ↥s] (h : s.finite) :
h.to_finset.card = fintype.card ↥s
source
theorem set.card_ne_eq {α : Type u} [fintype α] (a : α) [fintype ↥{x : α | x ≠ a}] :
fintype.card ↥{x : α | x ≠ a} = fintype.card α - 1

Infinite sets #

source
theorem set.infinite_univ_iff {α : Type u} :
set.univ.infinite ↔ infinite α
source
theorem set.infinite_univ {α : Type u} [h : infinite α] :
set.univ.infinite
source
theorem set.infinite_coe_iff {α : Type u} {s : set α} :
infinite ↥s ↔ s.infinite
source
theorem set.infinite.to_subtype {α : Type u} {s : set α} :
s.infinite → infinite ↥s

Alias of the reverse direction of set.infinite_coe_iff.

source
noncomputable def set.infinite.nat_embedding {α : Type u} (s : set α) (h : s.infinite) :
ℕ ↪ ↥s

Embedding of ℕ into an infinite set.

Equations
source
theorem set.infinite.exists_subset_card_eq {α : Type u} {s : set α} (hs : s.infinite) (n : ℕ) :
∃ (t : finset α), ↑t ⊆ s ∧ t.card = n
source
theorem set.infinite_of_finite_compl {α : Type u} [infinite α] {s : set α} (hs : sᶜ.finite) :
s.infinite
source
theorem set.finite.infinite_compl {α : Type u} [infinite α] {s : set α} (hs : s.finite) :
sᶜ.infinite
source
@[protected]
theorem set.infinite.mono {α : Type u} {s t : set α} (h : s ⊆ t) :
s.infinite → t.infinite
source
theorem set.infinite.diff {α : Type u} {s t : set α} (hs : s.infinite) (ht : t.finite) :
(s \ t).infinite
source
@[simp]
theorem set.infinite_union {α : Type u} {s t : set α} :
(s ∪ t).infinite ↔ s.infinite ∨ t.infinite
source
theorem set.infinite.of_image {α : Type u} {β : Type v} (f : α → β) {s : set α} (hs : (f '' s).infinite) :
s.infinite
source
theorem set.infinite_image_iff {α : Type u} {β : Type v} {s : set α} {f : α → β} (hi : set.inj_on f s) :
(f '' s).infinite ↔ s.infinite
source
@[protected]
theorem set.infinite.image {α : Type u} {β : Type v} {s : set α} {f : α → β} (hi : set.inj_on f s) :
s.infinite → (f '' s).infinite

Alias of the reverse direction of set.infinite_image_iff.

source
@[protected]
theorem set.infinite.image2_left {α : Type u} {β : Type v} {γ : Type x} {f : α → β → γ} {s : set α} {t : set β} {b : β} (hs : s.infinite) (hb : b ∈ t) (hf : set.inj_on (λ (a : α), f a b) s) :
(set.image2 f s t).infinite
source
@[protected]
theorem set.infinite.image2_right {α : Type u} {β : Type v} {γ : Type x} {f : α → β → γ} {s : set α} {t : set β} {a : α} (ht : t.infinite) (ha : a ∈ s) (hf : set.inj_on (f a) t) :
(set.image2 f s t).infinite
source
theorem set.infinite_image2 {α : Type u} {β : Type v} {γ : Type x} {f : α → β → γ} {s : set α} {t : set β} (hfs : ∀ (b : β), b ∈ t → set.inj_on (λ (a : α), f a b) s) (hft : ∀ (a : α), a ∈ s → set.inj_on (f a) t) :
(set.image2 f s t).infinite ↔ s.infinite ∧ t.nonempty ∨ t.infinite ∧ s.nonempty
source
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) :
t.infinite
source
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
source
theorem set.infinite_range_of_injective {α : Type u} {β : Type v} [infinite α] {f : α → β} (hi : function.injective f) :
(set.range f).infinite
source
theorem set.infinite_of_injective_forall_mem {α : Type u} {β : Type v} [infinite α] {s : set β} {f : α → β} (hi : function.injective f) (hf : ∀ (x : α), f x ∈ s) :
s.infinite
source
theorem set.infinite.exists_not_mem_finset {α : Type u} {s : set α} (hs : s.infinite) (f : finset α) :
∃ (a : α) (H : a ∈ s), a ∉ f
source
theorem set.not_inj_on_infinite_finite_image {α : Type u} {β : Type v} {f : α → β} {s : set α} (h_inf : s.infinite) (h_fin : (f '' s).finite) :
¬set.inj_on f s

Order properties #

source
theorem set.infinite_of_forall_exists_gt {α : Type u} [preorder α] [nonempty α] {s : set α} (h : ∀ (a : α), ∃ (b : α) (H : b ∈ s), a < b) :
s.infinite
source
theorem set.infinite_of_forall_exists_lt {α : Type u} [preorder α] [nonempty α] {s : set α} (h : ∀ (a : α), ∃ (b : α) (H : b ∈ s), b < a) :
s.infinite
source
theorem set.finite_is_top (α : Type u_1) [partial_order α] :
{x : α | is_top x}.finite
source
theorem set.finite_is_bot (α : Type u_1) [partial_order α] :
{x : α | is_bot x}.finite
source
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
source
theorem set.finite.exists_lt_map_eq_of_forall_mem {α : Type u} {β : Type v} [linear_order α] [infinite α] {t : set β} {f : α → β} (hf : ∀ (a : α), f a ∈ t) (ht : t.finite) :
∃ (a b : α), a < b ∧ f a = f b
source
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 ∈ s → f a ≤ f b)
source
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 ∈ s → f b ≤ f a)
source
theorem set.exists_lower_bound_image {α : Type u} {β : Type v} [hα : nonempty α] [linear_order β] (s : set α) (f : α → β) (h : s.finite) :
∃ (a : α), ∀ (b : α), b ∈ s → f a ≤ f b
source
theorem set.exists_upper_bound_image {α : Type u} {β : Type v} [hα : nonempty α] [linear_order β] (s : set α) (f : α → β) (h : s.finite) :
∃ (a : α), ∀ (b : α), b ∈ s → f b ≤ f a
source
theorem set.finite.supr_binfi_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [preorder ι'] [nonempty ι'] [is_directed ι' has_le.le] [order.frame α] {s : set ι} (hs : s.finite) {f : ι → ι' → α} (hf : ∀ (i : ι), i ∈ s → monotone (f i)) :
(⨆ (j : ι'), ⨅ (i : ι) (H : i ∈ s), f i j) = ⨅ (i : ι) (H : i ∈ s), ⨆ (j : ι'), f i j
source
theorem set.finite.supr_binfi_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [preorder ι'] [nonempty ι'] [is_directed ι' (function.swap has_le.le)] [order.frame α] {s : set ι} (hs : s.finite) {f : ι → ι' → α} (hf : ∀ (i : ι), i ∈ s → antitone (f i)) :
(⨆ (j : ι'), ⨅ (i : ι) (H : i ∈ s), f i j) = ⨅ (i : ι) (H : i ∈ s), ⨆ (j : ι'), f i j
source
theorem set.finite.infi_bsupr_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [preorder ι'] [nonempty ι'] [is_directed ι' (function.swap has_le.le)] [order.coframe α] {s : set ι} (hs : s.finite) {f : ι → ι' → α} (hf : ∀ (i : ι), i ∈ s → monotone (f i)) :
(⨅ (j : ι'), ⨆ (i : ι) (H : i ∈ s), f i j) = ⨆ (i : ι) (H : i ∈ s), ⨅ (j : ι'), f i j
source
theorem set.finite.infi_bsupr_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [preorder ι'] [nonempty ι'] [is_directed ι' has_le.le] [order.coframe α] {s : set ι} (hs : s.finite) {f : ι → ι' → α} (hf : ∀ (i : ι), i ∈ s → antitone (f i)) :
(⨅ (j : ι'), ⨆ (i : ι) (H : i ∈ s), f i j) = ⨆ (i : ι) (H : i ∈ s), ⨅ (j : ι'), f i j
source
theorem supr_infi_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [nonempty ι'] [is_directed ι' has_le.le] [order.frame α] {f : ι → ι' → α} (hf : ∀ (i : ι), monotone (f i)) :
(⨆ (j : ι'), ⨅ (i : ι), f i j) = ⨅ (i : ι), ⨆ (j : ι'), f i j
source
theorem supr_infi_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [nonempty ι'] [is_directed ι' (function.swap has_le.le)] [order.frame α] {f : ι → ι' → α} (hf : ∀ (i : ι), antitone (f i)) :
(⨆ (j : ι'), ⨅ (i : ι), f i j) = ⨅ (i : ι), ⨆ (j : ι'), f i j
source
theorem infi_supr_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [nonempty ι'] [is_directed ι' (function.swap has_le.le)] [order.coframe α] {f : ι → ι' → α} (hf : ∀ (i : ι), monotone (f i)) :
(⨅ (j : ι'), ⨆ (i : ι), f i j) = ⨆ (i : ι), ⨅ (j : ι'), f i j
source
theorem infi_supr_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [nonempty ι'] [is_directed ι' has_le.le] [order.coframe α] {f : ι → ι' → α} (hf : ∀ (i : ι), antitone (f i)) :
(⨅ (j : ι'), ⨆ (i : ι), f i j) = ⨆ (i : ι), ⨅ (j : ι'), f i j
source
theorem set.Union_Inter_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [is_directed ι' has_le.le] [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.

source
theorem set.Union_Inter_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [is_directed ι' (function.swap has_le.le)] [nonempty ι'] {s : ι → ι' → set α} (hs : ∀ (i : ι), antitone (s i)) :
(⋃ (j : ι'), ⋂ (i : ι), s i j) = ⋂ (i : ι), ⋃ (j : ι'), s i j

A decreasing union distributes over finite intersection.

source
theorem set.Inter_Union_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [is_directed ι' (function.swap has_le.le)] [nonempty ι'] {s : ι → ι' → set α} (hs : ∀ (i : ι), monotone (s i)) :
(⋂ (j : ι'), ⋃ (i : ι), s i j) = ⋃ (i : ι), ⋂ (j : ι'), s i j

An increasing intersection distributes over finite union.

source
theorem set.Inter_Union_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [is_directed ι' has_le.le] [nonempty ι'] {s : ι → ι' → set α} (hs : ∀ (i : ι), antitone (s i)) :
(⋂ (j : ι'), ⋃ (i : ι), s i j) = ⋃ (i : ι), ⋂ (j : ι'), s i j

A decreasing intersection distributes over finite union.

source
theorem set.Union_pi_of_monotone {ι : Type u_1} {ι' : Type u_2} [linear_order ι'] [nonempty ι'] {α : ι → Type u_3} {I : set ι} {s : Π (i : ι), ι' → set (α i)} (hI : I.finite) (hs : ∀ (i : ι), i ∈ I → monotone (s i)) :
(⋃ (j : ι'), I.pi (λ (i : ι), s i j)) = I.pi (λ (i : ι), ⋃ (j : ι'), s i j)
source
theorem set.Union_univ_pi_of_monotone {ι : Type u_1} {ι' : Type u_2} [linear_order ι'] [nonempty ι'] [finite ι] {α : ι → Type u_3} {s : Π (i : ι), ι' → set (α i)} (hs : ∀ (i : ι), monotone (s i)) :
(⋃ (j : ι'), set.univ.pi (λ (i : ι), s i j)) = set.univ.pi (λ (i : ι), ⋃ (j : ι'), s i j)
source
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
source
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' ∈ s → f a ≤ f a' → f a = f a')
source
@[protected]
theorem set.finite.bdd_above {α : Type u} [semilattice_sup α] [nonempty α] {s : set α} (hs : s.finite) :
bdd_above s

A finite set is bounded above.

source
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 ∈ I → bdd_above (S i)

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

source
theorem set.infinite_of_not_bdd_above {α : Type u} [semilattice_sup α] [nonempty α] {s : set α} :
¬bdd_above s → s.infinite
source
@[protected]
theorem set.finite.bdd_below {α : Type u} [semilattice_inf α] [nonempty α] {s : set α} (hs : s.finite) :
bdd_below s

A finite set is bounded below.

source
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 ∈ I → bdd_below (S i)

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

source
theorem set.infinite_of_not_bdd_below {α : Type u} [semilattice_inf α] [nonempty α] {s : set α} :
¬bdd_below s → s.infinite
source
@[protected]
theorem finset.bdd_above {α : Type u} [semilattice_sup α] [nonempty α] (s : finset α) :
bdd_above ↑s

A finset is bounded above.

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

A finset is bounded below.

source
theorem finite.of_forall_not_lt_lt {α : Type u} [linear_order α] (h : ∀ ⦃x y z : α⦄, x < y → y < z → false) :
finite α

If a linear order does not contain any triple of elements x < y < z, then this type is finite.

source
theorem set.finite_of_forall_not_lt_lt {α : Type u} [linear_order α] {s : set α} (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∀ (z : α), z ∈ s → x < y → y < z → false) :
s.finite

If a set s does not contain any triple of elements x < y < z, then s is finite.

source
theorem set.finite_diff_Union_Ioo {α : Type u} [linear_order α] (s : set α) :
(s \ ⋃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), set.Ioo x y).finite
source
theorem set.finite_diff_Union_Ioo' {α : Type u} [linear_order α] (s : set α) :
(s \ ⋃ (x : ↥s × ↥s), set.Ioo ↑(x.fst) ↑(x.snd)).finite