English
The copy operation creates a LieSubmodule with a prescribed carrier equal to a given set, preserving all structural properties.
Русский
Операция copy создаёт подмодуль Ли с заданным носителем равным заданному множеству, сохраняя все свойства структуры.
LaTeX
$$copy (s : Set M) (hs : s = ↑N) : LieSubmodule R L M$$
Lean4
/-- Copy of a `LieSubmodule` with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (s : Set M) (hs : s = ↑N) : LieSubmodule R L M
where
carrier := s
zero_mem' := by simp [hs]
add_mem' x y := by rw [hs] at x y ⊢; exact N.add_mem' x y
smul_mem' := by exact hs.symm ▸ N.smul_mem'
lie_mem := by exact hs.symm ▸ N.lie_mem
