range_eq_top_of_surjective

Mathlib.Algebra.Module.Submodule.Range

URI: https://scilib.ai/kg/mathlib#LinearMap.range_eq_top_of_surjective

English

The membership lemma for range: f(x) ∈ range f for any x.

Русский

Лемма принадлежности: f(x) ∈ range f для любого x.

LaTeX

$$$ f(x) \in \operatorname{range} f $$$

Lean4

theorem range_eq_top_of_surjective [RingHomSurjective τ₁₂] (f : F) (hf : Surjective f) : range f = ⊤ :=
  range_eq_top.2 hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru