English
Let f be a covering map. If g1,g2: A→E are continuous and f∘g1 = f∘g2, and there exists a ∈ A with g1(a)=g2(a), then g1=g2 on all of A.
Русский
Пусть f — покровное отображение. Если g1,g2: A→E непрерывны и f∘g1 = f∘g2, и существует a ∈ A такое, что g1(a)=g2(a), тогда g1=g2 на всём A.
LaTeX
$$$\text{Let } f:\, E\to X \text{ be a covering map. If } g_1,g_2:\, A\to E \text{ are continuous and } f\circ g_1=f\circ g_2, \exists a\in A: g_1(a)=g_2(a) \Rightarrow g_1=g_2.$$$
Lean4
theorem eq_of_comp_eq [PreconnectedSpace A] (h₁ : Continuous g₁) (h₂ : Continuous g₂) (he : f ∘ g₁ = f ∘ g₂) (a : A)
(ha : g₁ a = g₂ a) : g₁ = g₂ :=
hf.isSeparatedMap.eq_of_comp_eq hf.isLocalHomeomorph.isLocallyInjective h₁ h₂ he a ha
