range_eq_top — Mathlib

English

For a LieModuleHom f: M →ₗ⁅R,L⁆ N, the range equals the top submodule (i.e., the whole codomain) if and only if f is surjective.

Русский

Для гомоморфа Ли-модуля f: M →ₗ⁅R,L⁆ N образ равен сверху (то есть равен всему кодируемому модулю) тогда и только тогда, когда f сюръективен.

LaTeX

$$$f.range = \top \iff \text{Surjective}(f)$$$

Lean4

theorem range_eq_top : f.range = ⊤ ↔ Function.Surjective f := by
  rw [SetLike.ext'_iff, coe_range, LieSubmodule.top_coe, Set.range_eq_univ]

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