English
Given a sublattice L and a set s with hs : s = carrier(L), the construction L.copy s hs yields a sublattice whose carrier is s, transporting the closure properties from L along the equality hs.
Русский
Пусть L — подрешетка, и дано множество s такое, что hs: s = носитель(L). Тогда L.copy s hs образует подрешетку с носителем s, для которого замкнутость по объединению и пересечению перенесена из L вдоль равенства hs.
LaTeX
$$$ \\text{carrier}(L.copy\\, s\\, hs) = s \\quad \\land\\quad \\text{SupClosed}(L.copy\\, s\\, hs) = hs^{-1} \\cdot L.supClosed' \\land\\quad \\text{InfClosed}(L.copy\\, s\\, hs) = hs^{-1} \\cdot L.infClosed' $$$$
Lean4
/-- Copy of a sublattice with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (L : Sublattice α) (s : Set α) (hs : s = L) : Sublattice α
where
carrier := s
supClosed' := hs.symm ▸ L.supClosed'
infClosed' := hs.symm ▸ L.infClosed'
