eq_top_iff — Mathlib

English

Let S be a nonunital subalgebra of A over R. Then S equals the top subalgebra ⊤ if and only if every element of A belongs to S.

Русский

Пусть S — неединичная подпалгебра A над R. Тогда S = ⊤ тогда и только тогда, когда каждый элемент A принадлежит S.

LaTeX

$$$S = \\top \\iff \\forall x \\in A,\ x \\in S$$$

Lean4

theorem eq_top_iff {S : NonUnitalSubalgebra 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⟩⟩

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