map_top — Mathlib

English

For any nonunital algebra hom f: A →ₙₐ[R] B, the image of the top subalgebra ⊤ of A under f is exactly the range of f.

Русский

Для любого гомоморфа f: A →ₙₐ[R] B образ ⊤ в A под действием f равен образу f

LaTeX

$$$(\top : NonUnitalSubalgebra R A).map f = \operatorname{range}(f)$$$

Lean4

@[simp]
theorem map_top (f : A →ₙₐ[R] B) : (⊤ : NonUnitalSubalgebra R A).map f = NonUnitalAlgHom.range f :=
  SetLike.coe_injective Set.image_univ

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