finsetSup'_mem_supClosure — Mathlib

English

The supremum-closure of a finite set is finite.

Русский

Обобщение подмножества до верхней грани от конечного множества тоже конечное.

LaTeX

$$$s\\ \text{finite} \\Rightarrow (\\operatorname{supClosure}(s))\\ \text{finite}$$$

Lean4

theorem finsetSup'_mem_supClosure {ι : Type*} {t : Finset ι} (ht : t.Nonempty) {f : ι → α} (hf : ∀ i ∈ t, f i ∈ s) :
    t.sup' ht f ∈ supClosure s :=
  supClosed_supClosure.finsetSup'_mem _ fun _i hi ↦ subset_supClosure <| hf _ hi

Похожие утверждения