subsingleton_of_subsingleton — Mathlib

English

If A is a subsingleton, then there is a unique NonUnitalStarSubalgebra R A; equivalently, any two such subalgebras are equal.

Русский

Пусть A — множество с одним элементом. Тогда существует единственная подпалгебра без единицы над R в A; эквивалентно, любые две такие подпалгебры совпадают.

LaTeX

$$$\\forall S,T : \\mathrm{NonUnitalStarSubalgebra}\\,R\\,A,\\; S = T$$$

Lean4

instance subsingleton_of_subsingleton [Subsingleton A] : Subsingleton (NonUnitalStarSubalgebra R A) :=
  ⟨fun B C => ext fun x => by simp only [Subsingleton.elim x 0, zero_mem B, zero_mem C]⟩

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