English
The supremum-closure operator on sets (finite sets) yields another finite set when the input is finite.
Русский
Оператор supClosure применимый к конечному множеству даёт другое конечное множество.
LaTeX
$$$s \\text{ finite} \\Rightarrow (\\operatorname{supClosure}(s)).\\finite$$$
Lean4
/-- The semilattice generated by a finite set is finite. -/
protected theorem supClosure (hs : s.Finite) : (supClosure s).Finite :=
by
lift s to Finset α using hs
classical
refine ({t ∈ s.powerset | t.Nonempty}.attach.image fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
rintro _ ⟨t, ht, hts, rfl⟩
simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists, Finset.mem_powerset,
mem_filter]
exact ⟨t, ⟨hts, ht⟩, rfl⟩
