English
There exists an induction principle for latticeClosure over sup and inf. If a predicate p holds for elements of s and is preserved under sup and inf within latticeClosure(s), then p holds for all elements of latticeClosure(s).
Русский
Существует принцип индукции для latticeClosure по операциям объединения и пересечения: если свойство выполняется для элементов s и сохраняется при объединении и пересечении внутри latticeClosure(s), то выполняется для всех элементов latticeClosure(s).
LaTeX
$$$\text{Induction on } \mathrm{latticeClosure}(s):\;\forall p:(\alpha\to\mathrm{Prop})\to (\ldots) \Rightarrow (\ldots) \Rightarrow \forall a\in \mathrm{latticeClosure}(s),\ p\ a\ (\ldots)$$$
Lean4
theorem latticeClosure_min : s ⊆ t → IsSublattice t → latticeClosure s ⊆ t :=
latticeClosure.closure_min
