instNontrivialSubtypeMemOfIsCartanSubalgebra

English

There exists a nontrivial element in the subobject representing a Cartan subalgebra.

Русский

Существует ненулевой элемент внутри подобъекта, представляющего Картанову подалгебру.

LaTeX

$$$\\text{Nontrivial}(\\text{Subtype }\\;\\{x: L\\mid x\\in H\\})$$$

Lean4

instance (priority := 500) [Nontrivial L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] : Nontrivial H :=
  by
  refine (subsingleton_or_nontrivial H).elim (fun inst ↦ False.elim ?_) id
  apply ne_bot_of_isCartanSubalgebra H
  rw [eq_bot_iff]
  exact fun x hx ↦ congr_arg Subtype.val (Subsingleton.elim (⟨x, hx⟩ : H) 0)

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