English
The inf-closure distributes over Cartesian product: infClosure(s × t) = infClosure(s) × infClosure(t).
Русский
Замыкание по inf распределяется по произведению: infClosure(s × t) = infClosure(s) × infClosure(t).
LaTeX
$$$\infClosure(s \times\, t) = \infClosure(s) \times\, \infClosure(t)$$$
Lean4
/-- The semilattice generated by a finite set is finite. -/
protected theorem infClosure (hs : s.Finite) : (infClosure s).Finite :=
by
lift s to Finset α using hs
classical
refine ({t ∈ s.powerset | t.Nonempty}.attach.image fun t ↦ t.1.inf' (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⟩
