eq_top_iff — Mathlib

English

For any StarSubalgebra S of A, S = ⊤ if and only if every element of A lies in S.

Русский

Для любого StarSubalgebra S ⊆ A верно: S = ⊤ тогда и только тогда, когда каждый элемент A принадлежит S.

LaTeX

$$$ S = \\top \\;\\Longleftrightarrow\\; \\forall x:\\,A,\\; x \\in S $$$

Lean4

theorem eq_top_iff {S : StarSubalgebra R A} : S = ⊤ ↔ ∀ x : A, x ∈ S :=
  ⟨fun h x => by rw [h]; exact mem_top, fun h => by ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩⟩

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