isLocallyInjective_iff_nhds — Mathlib

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⟩

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