data.set.finite - mathlib3 docs

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

h.fintype = _.some

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

h.to_finset = s.to_finset

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

set.finite.can_lift = {prf := _}

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

s.infinite = ¬s.finite

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

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

source

@[protected, instance]

def set.fintype_univ {α : Type u} [fintype α] :

fintype ↥set.univ

Equations

set.fintype_univ = fintype.of_equiv α (equiv.set.univ α).symm

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

set.fintype_of_finite_univ H = fintype.of_equiv ↥set.univ (equiv.set.univ α)

source

@[protected, instance]

def set.fintype_union {α : Type u} [decidable_eq α] (s t : set α) [fintype ↥s] [fintype ↥t] :

fintype ↥(s ∪ t)

Equations

s.fintype_union t = fintype.of_finset (s.to_finset ∪ t.to_finset) _

source

@[protected, instance]

def set.fintype_sep {α : Type u} (s : set α) (p : α → Prop) [fintype ↥s] [decidable_pred p] :

fintype ↥{a ∈ s | p a}

Equations

s.fintype_sep p = fintype.of_finset (finset.filter p s.to_finset) _

source

@[protected, instance]

def set.fintype_inter {α : Type u} (s t : set α) [decidable_eq α] [fintype ↥s] [fintype ↥t] :

fintype ↥(s ∩ t)

Equations

s.fintype_inter t = fintype.of_finset (s.to_finset ∩ t.to_finset) _

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

s.fintype_inter_of_left t = fintype.of_finset (finset.filter (λ (_x : α), _x ∈ t) s.to_finset) _

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

s.fintype_inter_of_right t = fintype.of_finset (finset.filter (λ (_x : α), _x ∈ s) t.to_finset) _

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

s.fintype_subset h = _.mpr (s.fintype_inter_of_left t)

source

@[protected, instance]

def set.fintype_diff {α : Type u} [decidable_eq α] (s t : set α) [fintype ↥s] [fintype ↥t] :

fintype ↥(s \ t)

Equations

s.fintype_diff t = fintype.of_finset (s.to_finset \ t.to_finset) _

source

@[protected, instance]

def set.fintype_diff_left {α : Type u} (s t : set α) [fintype ↥s] [decidable_pred (λ (_x : α), _x ∈ t)] :

fintype ↥(s \ t)

Equations

s.fintype_diff_left t = s.fintype_sep (λ (_x : α), _x ∈ tᶜ)

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

set.fintype_Union f = fintype.of_finset (finset.univ.bUnion (λ (i : plift ι), (f i.down).to_finset)) _

source

@[protected, instance]

def set.fintype_sUnion {α : Type u} [decidable_eq α] {s : set (set α)} [fintype ↥s] [H : Π (t : ↥s), fintype ↥↑t] :

fintype (↥⋃₀ s)

Equations

set.fintype_sUnion = set.fintype_sUnion._proof_1.mpr (set.fintype_Union (λ (t : ↥s), ↑t))

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

s.fintype_bUnion t H = fintype.of_finset (s.to_finset.attach.bUnion (λ (x : {x // x ∈ s.to_finset}), (t ↑x).to_finset)) _

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

s.fintype_bUnion' t = fintype.of_finset (s.to_finset.bUnion (λ (x : ι), (t x).to_finset)) _

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

s.fintype_bind f H = s.fintype_bUnion f H

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

s.fintype_bind' f = s.fintype_bUnion' f

source

@[protected, instance]

def set.fintype_empty {α : Type u} :

fintype ↥∅

Equations

set.fintype_empty = fintype.of_finset ∅ set.fintype_empty._proof_1

source

@[protected, instance]

def set.fintype_singleton {α : Type u} (a : α) :

fintype ↥{a}

Equations

set.fintype_singleton a = fintype.of_finset {a} _

source

@[protected, instance]

def set.fintype_pure {α : Type u} (a : α) :

fintype ↥(has_pure.pure a)

Equations

set.fintype_pure = set.fintype_singleton

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

set.fintype_insert a s = fintype.of_finset (has_insert.insert a s.to_finset) _

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

s.fintype_insert_of_not_mem h = fintype.of_finset {val := a ::ₘ s.to_finset.val, nodup := _} _

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

s.fintype_insert_of_mem h = fintype.of_finset s.to_finset _

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

set.fintype_insert' a s = dite (a ∈ s) (λ (h : a ∈ s), s.fintype_insert_of_mem h) (λ (h : a ∉ s), s.fintype_insert_of_not_mem h)

source

@[protected, instance]

def set.fintype_image {α : Type u} {β : Type v} [decidable_eq β] (s : set α) (f : α → β) [fintype ↥s] :

fintype ↥(f '' s)

Equations

s.fintype_image f = fintype.of_finset (finset.image f s.to_finset) _

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

s.fintype_of_fintype_image I = fintype.of_finset {val := multiset.filter_map g (f '' s).to_finset.val, nodup := _} _

source

@[protected, instance]

def set.fintype_range {α : Type u} {ι : Sort w} [decidable_eq α] (f : ι → α) [fintype (plift ι)] :

fintype ↥(set.range f)

Equations

set.fintype_range f = fintype.of_finset (finset.image (f ∘ plift.down) finset.univ) _

source

@[protected, instance]

def set.fintype_map {α β : Type u_1} [decidable_eq β] (s : set α) (f : α → β) [fintype ↥s] :

fintype ↥(f <$> s)

Equations

set.fintype_map = set.fintype_image

source

@[protected, instance]

def set.fintype_lt_nat (n : ℕ) :

fintype ↥{i : ℕ | i < n}

Equations

set.fintype_lt_nat n = fintype.of_finset (finset.range n) _

source

@[protected, instance]

def set.fintype_le_nat (n : ℕ) :

fintype ↥{i : ℕ | i ≤ n}

Equations

set.fintype_le_nat n = _.mpr (_.mp (set.fintype_lt_nat (n + 1)))

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

set.nat.fintype_Iio n = set.fintype_lt_nat n

source

@[protected, instance]

def set.fintype_prod {α : Type u} {β : Type v} (s : set α) (t : set β) [fintype ↥s] [fintype ↥t] :

fintype ↥(s ×ˢ t)

Equations

s.fintype_prod t = fintype.of_finset (s.to_finset ×ˢ t.to_finset) _

source

@[protected, instance]

def set.fintype_off_diag {α : Type u} [decidable_eq α] (s : set α) [fintype ↥s] :

fintype ↥(s.off_diag)

Equations

s.fintype_off_diag = fintype.of_finset s.to_finset.off_diag _

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

set.fintype_image2 f s t = _.mpr ((s ×ˢ t).fintype_image (λ (x : α × β), f x.fst x.snd))

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

f.fintype_seq s = _.mpr (f.fintype_bUnion' (λ (x : α → β), x '' s))

source

@[protected, instance]

def set.fintype_seq' {α β : Type u} [decidable_eq β] (f : set (α → β)) (s : set α) [fintype ↥f] [fintype ↥s] :

fintype ↥(f <*> s)

Equations

f.fintype_seq' s = f.fintype_seq s

source

@[protected, instance]

def set.fintype_mem_finset {α : Type u} (s : finset α) :

fintype ↥{a : α | a ∈ s}

Equations

set.fintype_mem_finset s = s.fintype_coe_sort

source

theorem equiv.set_finite_iff {α : Type u} {β : Type v} {s : set α} {t : set β} (hst : ↥s ≃ ↥t) :

s.finite ↔ t.finite

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

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)

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

source

@[protected, instance]

def set.finite.inhabited {α : Type u} :

inhabited {s // s.finite}

Equations

set.finite.inhabited = {default := ⟨∅, _⟩}

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

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

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

set.infinite.nat_embedding s h = infinite.nat_embedding ↥s

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

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} [preorder α] [is_directed α has_le.le] [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} [preorder α] [is_directed α has_le.le] [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} [preorder α] [is_directed α has_le.le] [nonempty α] {s : set α} :

¬bdd_above s → s.infinite

source

@[protected]

theorem set.finite.bdd_below {α : Type u} [preorder α] [is_directed α ge] [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} [preorder α] [is_directed α ge] [nonempty α] {I : set β} {S : β → set α} (H : I.finite) :