mem_range_iff_of_surjective — Mathlib

English

Let f: X → S and g: Y → S be morphisms with e: X → Y surjective and f = e ≫ g. Then for any s ∈ S, s belongs to the range of f_base if and only if s belongs to the range of g_base.

Русский

Пусть f: X → S и g: Y → S — морфизмы, e: X → Y сюръективно, и f = e ≫ g. Тогда для любого s ∈ S: s принадлежит диапазону f_base тогда и только тогда, когда принадлежит диапазону g_base.

LaTeX

$$$\forall s:\, S,\ s \in \operatorname{range}(f_{\mathrm{base}}) \iff s \in \operatorname{range}(g_{\mathrm{base}})$$$

Lean4

theorem mem_range_iff_of_surjective {S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) (e : X ⟶ Y) [Surjective e]
    (hge : e ≫ g = f) (s : S) : s ∈ Set.range f.base ↔ s ∈ Set.range g.base := by
  rw [range_eq_range_of_surjective f g e hge]

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