English
For a morphism f with P respecting Iso, sourceLocalClosure IsOpenImmersion P f holds iff every point x ∈ X has an open neighborhood U with x ∈ U and P (U ι ≫ f).
Русский
Для морфизма f с соблюдением изоморфизмов sourceLocalClosure IsOpenImmersion P f эквивалентно тому, что для каждой точки x ∈ X существует открытое окрестность U с x ∈ U и P (U ι ≫ f).
LaTeX
$$sourceLocalClosure IsOpenImmersion P f ↔ ∀ x ∈ X, ∃ U ∈ Opens, x ∈ U ∧ P (U.ι ≫ f)$$
Lean4
theorem iff_forall_exists [P.RespectsIso] {f : X ⟶ Y} :
sourceLocalClosure IsOpenImmersion P f ↔ ∀ (x : X), ∃ (U : X.Opens), x ∈ U ∧ P (U.ι ≫ f) :=
by
refine ⟨fun ⟨𝒰, hf⟩ x ↦ ?_, fun H ↦ ?_⟩
· refine ⟨(𝒰.f (𝒰.idx x)).opensRange, 𝒰.covers x, ?_⟩
rw [← Scheme.Hom.isoOpensRange_inv_comp, Category.assoc, P.cancel_left_of_respectsIso]
apply hf
· choose U hx hf using H
exact ⟨.mkOfCovers X (fun x ↦ U x) (fun _ ↦ (U _).ι) (fun x ↦ ⟨x, ⟨x, hx x⟩, rfl⟩) fun _ ↦ inferInstance, hf⟩
