English
Lie subalgebras with equal underlying sets are isomorphic as Lie algebras via the identity on the common set.
Русский
Подалгебры Ли, имеющие одинаковые основания как множества, изоморфны как алгебры Ли через тождественное отображение на общем множестве.
LaTeX
$$$L_1' \\cong_R L_1'' \\quad\\text{if } (L_1':L_1)=(L_1'':L_1)\\\\$$
Lean4
/-- Lie subalgebras that are equal as sets are equivalent as Lie algebras. -/
def ofEq (h : (L₁' : Set L₁) = L₁'') : L₁' ≃ₗ⁅R⁆ L₁'' :=
{
LinearEquiv.ofEq (L₁' : Submodule R L₁) (L₁'' : Submodule R L₁)
(by
ext x
change x ∈ (L₁' : Set L₁) ↔ x ∈ (L₁'' : Set L₁)
rw [h]) with
map_lie' {_ _} := rfl }
