injective_isZariskiLocalAtTarget — Mathlib

English

The property that a map is injective on underlying topological spaces is Zariski-local at the target.

Русский

Свойство инъективности в топологическом основании локально по зарискам на цели.

LaTeX

$$injective_isZariskiLocalAtTarget$$

Lean4

instance injective_isZariskiLocalAtTarget : IsZariskiLocalAtTarget (topologically Function.Injective) :=
  by
  refine topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s) fun f ι U H _ hf x₁ x₂ e ↦ ?_
  obtain ⟨i, hxi⟩ : ∃ i, f x₁ ∈ U i := by simpa using congr(f x₁ ∈ $H)
  exact congr(($(@hf i ⟨x₁, hxi⟩ ⟨x₂, show f x₂ ∈ U i from e ▸ hxi⟩ (Subtype.ext e))).1)

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