English
IsLocallyInjective f is equivalent to the diagonal pullback being open in the appropriate product space.
Русский
Локальная инъективность f эквивалентна тому, что диагональная подмножество открыто в произведении пространств.
LaTeX
$$IsLocallyInjective f \iff IsOpen (pullbackDiagonal f)$$
Lean4
theorem isLocallyInjective_iff_isOpen_diagonal {f : X → Y} : IsLocallyInjective f ↔ IsOpen f.pullbackDiagonal :=
by
simp_rw [isLocallyInjective_iff_nhds, isOpen_iff_mem_nhds, Subtype.forall, Prod.forall, nhds_induced, nhds_prod_eq,
Filter.mem_comap]
refine ⟨?_, fun h x ↦ ?_⟩
· rintro h x x' hx (rfl : x = x')
obtain ⟨U, hn, hi⟩ := h x
exact ⟨_, Filter.prod_mem_prod hn hn, fun {p} hp ↦ hi hp.1 hp.2 p.2⟩
· obtain ⟨t, ht, t_sub⟩ := h x x rfl rfl
obtain ⟨t₁, h₁, t₂, h₂, prod_sub⟩ := Filter.mem_prod_iff.mp ht
exact ⟨t₁ ∩ t₂, Filter.inter_mem h₁ h₂, fun x₁ h₁ x₂ h₂ he ↦ @t_sub ⟨(x₁, x₂), he⟩ (prod_sub ⟨h₁.1, h₂.2⟩)⟩
