The sup-closure of an indexed family #
[UPSTREAM] candidate for Mathlib/Order/SupClosed.lean.
The sup-closure of the image of a set of indices is the set of sups of the family over the nonempty finite sets of those indices, and dually for the inf-closure. For a family of sets these are the unions and the intersections of its members over nonempty finite sets of indices. Closing a set under sups does not change its infimum, nor closing it under infs its supremum.
Main results #
mem_supClosure_image,mem_infClosure_image: membership in the closure of an image.Set.mem_supClosure_image,Set.mem_infClosure_image: the same for a family of sets.sInf_supClosure,sSup_infClosure: the closures keep the infimum and the supremum.
theorem
mem_supClosure_image
{ι : Type u_1}
{α : Type u_2}
[SemilatticeSup α]
{f : ι → α}
{s : Set ι}
{a : α}
:
a ∈ supClosure (f '' s) ↔ ∃ (t : Finset ι) (ht : t.Nonempty), ↑t ⊆ s ∧ t.sup' ht f = a
theorem
mem_infClosure_image
{ι : Type u_1}
{α : Type u_2}
[SemilatticeInf α]
{f : ι → α}
{s : Set ι}
{a : α}
:
a ∈ infClosure (f '' s) ↔ ∃ (t : Finset ι) (ht : t.Nonempty), ↑t ⊆ s ∧ t.inf' ht f = a
theorem
sInf_supClosure
{α : Type u_2}
[CompleteLattice α]
(s : Set α)
:
sInf (supClosure s) = sInf s
theorem
sSup_infClosure
{α : Type u_2}
[CompleteLattice α]
(s : Set α)
:
sSup (infClosure s) = sSup s
theorem
Set.mem_supClosure_image
{ι : Type u_1}
{W : Type u_3}
{f : ι → Set W}
{s : Set ι}
{q : Set W}
:
q ∈ supClosure (f '' s) ↔ ∃ (t : Finset ι), t.Nonempty ∧ ↑t ⊆ s ∧ ⋃ i ∈ t, f i = q
theorem
Set.mem_infClosure_image
{ι : Type u_1}
{W : Type u_3}
{f : ι → Set W}
{s : Set ι}
{q : Set W}
:
q ∈ infClosure (f '' s) ↔ ∃ (t : Finset ι), t.Nonempty ∧ ↑t ⊆ s ∧ ⋂ i ∈ t, f i = q
theorem
Set.mem_supClosure_range
{ι : Type u_1}
{W : Type u_3}
{f : ι → Set W}
{q : Set W}
:
q ∈ supClosure (range f) ↔ ∃ (t : Finset ι), t.Nonempty ∧ ⋃ i ∈ t, f i = q
theorem
Set.mem_infClosure_range
{ι : Type u_1}
{W : Type u_3}
{f : ι → Set W}
{q : Set W}
:
q ∈ infClosure (range f) ↔ ∃ (t : Finset ι), t.Nonempty ∧ ⋂ i ∈ t, f i = q
theorem
Set.supClosure_range_eq_image
{ι : Type u_1}
{W : Type u_3}
{f : ι → Set W}
:
supClosure (range f) = (fun (t : Finset ι) => ⋃ i ∈ t, f i) '' {t : Finset ι | t.Nonempty}
theorem
Set.infClosure_range_eq_image
{ι : Type u_1}
{W : Type u_3}
{f : ι → Set W}
:
infClosure (range f) = (fun (t : Finset ι) => ⋂ i ∈ t, f i) '' {t : Finset ι | t.Nonempty}