of_discreteTopology — Mathlib

English

If both domain E and codomain X are equipped with discrete topology, then any map f: E → X is a covering map.

Русский

Если и область определения E, и кодомен X имеют дискретную топологию, то любая функция f: E → X является покрытием.

LaTeX

$$$ \text{IsCoveringMap } f $, при дискретной топологии на E и X.$$

Lean4

theorem of_discreteTopology [DiscreteTopology E] [DiscreteTopology X] : IsCoveringMap f := fun x ↦
  ⟨inferInstance, { x }, rfl, isOpen_discrete _, isOpen_discrete _,
    { toFun e := ⟨⟨x, rfl⟩, e⟩
      invFun xi := xi.2
      left_inv _ := rfl
      right_inv _ := Prod.ext (Subsingleton.elim ..) rfl }, (·.2.symm)⟩

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