English
The LieIdeals of the bottom LieAlgebra ⊥ form a singleton: there is only one LieIdeal in ⊥.
Русский
Ли-идеалы нулевой подалгебры ⊥ образуют сепаратный набор: существует единственный Ли-идеал внутри ⊥.
LaTeX
$$Subsingleton (LieIdeal R (⊥ : LieIdeal R L))$$
Lean4
theorem map_of_image (h : f '' I = J) : I.map f = J :=
by
apply le_antisymm
· rw [map, LieSubmodule.lieSpan_le, Submodule.map_coe]
/- I'm uncertain how to best resolve this `erw`.
```
have : (↑(toLieSubalgebra R L I).toSubmodule : Set L) = I := rfl
rw [this]
simp [h]
```
works, but still feels awkward. There are missing `simp` lemmas here.`
-/
erw [h]
· rw [← SetLike.coe_subset_coe, ← h]; exact LieSubmodule.subset_lieSpan
