subsingleton_of_bot — Mathlib

English

The bottom Lie subalgebra (as a subobject) is a subsingleton.

Русский

Нижняя подалгебра как объект обладает единственным элементом.

LaTeX

$$$ Subsingleton (\\mathrm{LieSubalgebra}_R (\\perp : \\mathrm{LieSubalgebra}_R L))$$$

Lean4

instance subsingleton_of_bot : Subsingleton (LieSubalgebra R (⊥ : LieSubalgebra R L)) :=
  by
  apply subsingleton_of_bot_eq_top
  ext ⟨x, hx⟩; change x ∈ ⊥ at hx; rw [LieSubalgebra.mem_bot] at hx; subst hx
  simp only [mem_bot, mem_top, iff_true]
  rfl

Похожие утверждения