range_eq_top — Mathlib

English

A variant statement asserting the same range-top relation for a similar setting of nonunital subalgebras and identity-like morphisms.

Русский

Вариант утверждения о той же связи образ-верхняя часть для аналогичной настройки подалгебр без единицы и идентного вида отображения.

LaTeX

$$$\text{(variant)}\; \operatorname{range}(f) = \top \;\iff \; \text{Surjective}(f)$$$

Lean4

theorem range_eq_top [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) :
    NonUnitalAlgHom.range f = (⊤ : NonUnitalSubalgebra R B) ↔ Function.Surjective f :=
  NonUnitalAlgebra.eq_top_iff

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