English
For a family of lattices α i, if each t i is a Sublattice, then s.pi t is a Sublattice.
Русский
Для семейства решеток α_i, если каждый t_i является субрешеткой, то s.pi t — субрешетка.
LaTeX
$$ (∀ i, IsSublattice (t i)) → IsSublattice (s.pi t)$$
Lean4
/-- Every set in a join-semilattice generates a set closed under join. -/
@[simps! isClosed]
def supClosure : ClosureOperator (Set α) :=
.ofPred (fun s ↦ {a | ∃ (t : Finset α) (ht : t.Nonempty), ↑t ⊆ s ∧ t.sup' ht id = a}) SupClosed
(fun s a ha ↦ ⟨{ a }, singleton_nonempty _, by simpa⟩)
(by
classical
rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
refine ⟨_, ht.mono subset_union_left, ?_, sup'_union ht hu _⟩
rw [coe_union]
exact Set.union_subset hts hus)
(by rintro s₁ s₂ hs h₂ _ ⟨t, ht, hts, rfl⟩; exact h₂.finsetSup'_mem ht fun i hi ↦ hs <| hts hi)
