English
Let s,t be subsets of a lattice α that are closed under finite joins and meets, so that they define sublattices S = ⟨s, hs_sup, hs_inf⟩ and T = ⟨t, ht_sup, ht_inf⟩. Then S < T in the sublattice order if and only if s ⊊ t.
Русский
Пусть s, t ⊆ α замкнуты относительно операций объединения и пересечения и определяют подрешетки S и T. Тогда S < T в порядке подрешеток тогда и только тогда, когда s является собственным подмножеством t.
LaTeX
$$$ mk \; s \; hs\_sup \; hs\_inf < mk \; t \; ht\_sup \; ht\_inf \\iff s \\subsetneq t $$$
Lean4
@[simp]
theorem mk_lt_mk (hs_sup hs_inf ht_sup ht_inf) : mk s hs_sup hs_inf < mk t ht_sup ht_inf ↔ s ⊂ t :=
Iff.rfl
