eq_top_iff — Mathlib

English

The range of a map equals the top subalgebra iff the map is surjective.

Русский

Образ отображения равен верхней подалгебре тогда и только тогда, когда отображение сюръективно.

LaTeX

$$$\\text{range } f = \\top \\; \\Leftrightarrow\\; \\text{Function.Surjective } f$$$

Lean4

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

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