English
If p is separated and locally injective, and two lifts g1,g2 have equal composites with p on a connected domain, then g1=g2 on the domain.
Русский
Если p разделяющее и локально инъективное, и две подстановки g1,g2 имеют равные композиции с p на связной области, то g1=g2 на всей области.
LaTeX
$$IsSeparatedMap p → IsLocallyInjective p → [PreconnectedSpace A] → Continuous g1 → Continuous g2 → Eq (p ∘ g1) (p ∘ g2) → ∀ a, Eq (g1 a) (g2 a)$$
Lean4
/-- If `p` is a locally injective separated map, and `A` is a connected space,
then two lifts `g₁, g₂ : A → E` of a map `f : A → X` are equal if they agree at one point. -/
theorem eq_of_comp_eq [PreconnectedSpace A] (h₁ : Continuous g₁) (h₂ : Continuous g₂) (he : p ∘ g₁ = p ∘ g₂) (a : A)
(ha : g₁ a = g₂ a) : g₁ = g₂ :=
funext fun a' ↦ by
apply (IsClopen.eq_univ ⟨sep.isClosed_eqLocus h₁ h₂ he, inj.isOpen_eqLocus h₁ h₂ he⟩ ⟨a, ha⟩).symm ▸ Set.mem_univ a'
