English
Let f be a covering map. If A is preconnected and g1,g2: A→E are continuous on a subset s, and f∘g1 and f∘g2 agree on s, then g1 and g2 agree on s.
Русский
Пусть f — покровное отображение. Пусть A предсоединённо, g1,g2: A→E непрерывны на s, и f∘g1 = f∘g2 на s. Тогда g1 = g2 на s.
LaTeX
$$$[\text{Preconnected}(s)]\ (h_1:\text{ContinuousOn}(g_1,s))\ (h_2:\text{ContinuousOn}(g_2,s))\ (he: (f\circ g_1)|_s=(f\circ g_2)|_s)\Rightarrow (g_1|_s=g_2|_s)$$$
Lean4
theorem eqOn_of_comp_eqOn (hs : IsPreconnected s) (h₁ : ContinuousOn g₁ s) (h₂ : ContinuousOn g₂ s)
(he : s.EqOn (f ∘ g₁) (f ∘ g₂)) {a : A} (has : a ∈ s) (ha : g₁ a = g₂ a) : s.EqOn g₁ g₂ :=
hf.isSeparatedMap.eqOn_of_comp_eqOn hf.isLocalHomeomorph.isLocallyInjective hs h₁ h₂ he has ha
