English
IsLocallyInjective f is equivalent to: for every x, there exists U ∈ nhds x such that U.InjOn f.
Русский
IsLocallyInjective f эквивалентно: для каждого x существует U ∈ nhds(x), такое что U.InjOn f.
LaTeX
$$IsLocallyInjective f \iff ∀ x, ∃ U ∈ nhds(x), U.InjOn f$$
Lean4
theorem isLocallyInjective_iff_nhds {f : X → Y} : IsLocallyInjective f ↔ ∀ x : X, ∃ U ∈ 𝓝 x, U.InjOn f :=
by
constructor <;> intro h x
· obtain ⟨U, ho, hm, hi⟩ := h x; exact ⟨U, ho.mem_nhds hm, hi⟩
· obtain ⟨U, hn, hi⟩ := h x
exact ⟨interior U, isOpen_interior, mem_interior_iff_mem_nhds.mpr hn, hi.mono interior_subset⟩