English
Let α be a complete lattice, and L a complete sublattice of α. For any subset s of α and any equality hs: s = carrier(L), the structure L.copy s hs is again a complete sublattice of α whose carrier is s.
Русский
Пусть α — полная решетка, и L — полная подпредложенная подрешетка α. Для любого множества s ⊆ α и равенства hs: s = носитель(L) образуется новая полная подпорелетка L.copy s hs, чья носитель равен s.
LaTeX
$$$L.copy\,s\,hs$$$
Lean4
/-- Copy of a complete sublattice with a new `carrier` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (s : Set α) (hs : s = L) : CompleteSublattice α :=
mk' s (hs ▸ L.sSupClosed') (hs ▸ L.sInfClosed')
