range_snd — Mathlib

English

Similarly, the range of the snd projection from the pullback equals the preimage in Y of the range of f.base in S.

Русский

Аналогично, область значений snd-проекции из pullback равна предобразу образа f.base в S по карте g.

LaTeX

$$$Set.range (pullback.snd f g).base = g.base^{-1}( Set.range f.base )$$$

Lean4

theorem range_snd : Set.range (pullback.snd f g).base = g.base ⁻¹' Set.range f.base :=
  by
  ext x
  refine ⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩
  · rintro ⟨a, rfl⟩
    simp only [Set.mem_preimage, Set.mem_range, ← Scheme.comp_base_apply, ← pullback.condition]
    simp
  · obtain ⟨a, ha⟩ := Triplet.exists_preimage (Triplet.mk' y x hy)
    use a, ha.right

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