English
A covering map is a separated map.
Русский
Покрывающее отображение является разделённым отображением.
LaTeX
$$$\forall f:\ E\to X,\ IsCoveringMap(f) \Rightarrow \text{IsSeparatedMap}(f)$$$
Lean4
protected theorem isSeparatedMap : IsSeparatedMap f := fun e₁ e₂ he hne ↦
by
have : Nonempty (f ⁻¹' {f e₁}) := ⟨⟨e₁, rfl⟩⟩
specialize hf (f e₁)
let t := hf.toTrivialization
have := hf.discreteTopology_fiber
have he₁ := hf.mem_toTrivialization_baseSet
have he₂ := he₁; simp_rw [he] at he₂; rw [← t.mem_source] at he₁ he₂
refine
⟨t.source ∩ (Prod.snd ∘ t) ⁻¹' {(t e₁).2}, t.source ∩ (Prod.snd ∘ t) ⁻¹' {(t e₂).2}, ?_, ?_, ⟨he₁, rfl⟩, ⟨he₂, rfl⟩,
Set.disjoint_left.mpr fun x h₁ h₂ ↦ hne (t.injOn he₁ he₂ ?_)⟩
iterate 2
exact
t.continuousOn_toFun.isOpen_inter_preimage t.open_source (continuous_snd.isOpen_preimage _ <| isOpen_discrete _)
refine Prod.ext ?_ (h₁.2.symm.trans h₂.2)
rwa [t.proj_toFun e₁ he₁, t.proj_toFun e₂ he₂]
