coe_bot — Mathlib

English

A subalgebra equals the top if and only if every element lies in it.

Русский

Подалгебра равна верхней, если и только если каждый элемент принадлежит ей.

LaTeX

$$$S = \\top \\;\\Leftrightarrow\\; \\forall x, x \\in S$$$

Lean4

@[simp, norm_cast]
theorem coe_bot : ((⊥ : NonUnitalStarSubalgebra R A) : Set A) = {0} := by
  simp only [Set.ext_iff, NonUnitalStarAlgebra.mem_bot, SetLike.mem_coe, Set.mem_singleton_iff, forall_const]

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