rangeS_top_iff_surjective

Mathlib.Algebra.Ring.Subsemiring.Basic

URI: https://scilib.ai/kg/mathlib#RingHom.rangeS_top_iff_surjective

← MathLib Explorer

English

The proposition that f.rangeS = ⊤ is equivalent to f being surjective.

Русский

Утверждение, что $f.rangeS=⊤$, эквивалентно сюръективности $f$.

LaTeX

$$$f.rangeS = \\top \\iff \\text{Function.Surjective} f$$$

Lean4

theorem rangeS_top_iff_surjective {f : R →+* S} : f.rangeS = (⊤ : Subsemiring S) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_rangeS, coe_top]) Set.range_eq_univ

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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