discreteTopology_iff_locallyInjective

English

In a discrete topology, every map is locally injective. Conversely, a discrete space implies local injectivity for maps into it.

Русский

В дискретном пространстве каждое отображение локально инъективно; наоборот, дискретность пространства обеспечивает локальную инъективность отображений в него.

LaTeX

$$DiscreteTopology X ∧ IsLocallyInjective f$$

Lean4

theorem discreteTopology_iff_locallyInjective (y : Y) : DiscreteTopology X ↔ IsLocallyInjective fun _ : X ↦ y :=
  by
  rw [discreteTopology_iff_singleton_mem_nhds, isLocallyInjective_iff_nhds]
  refine forall_congr' fun x ↦ ⟨fun h ↦ ⟨{ x }, h, Set.injOn_singleton _ _⟩, fun ⟨U, hU, inj⟩ ↦ ?_⟩
  convert hU; ext x'; refine ⟨?_, fun h ↦ inj h (mem_of_mem_nhds hU) rfl⟩
  rintro rfl; exact mem_of_mem_nhds hU

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