English
If p is separated and locally injective, and two maps g1,g2 agree after composing with p on a preconnected subset, then they agree on that subset.
Русский
Если p разделяющее и локально инъективное, и g1,g2 согласованы после композиции с p на предподсоединённом подмножестве, то они согласованы на этом подмножестве.
LaTeX
$$IsSeparatedMap p → IsLocallyInjective p → IsPreconnected s → ContinuousOn g1 s → ContinuousOn g2 s → s.EqOn (p ∘ g1) (p ∘ g2) → ∀ a ∈ s, Eq (g1 a) (g2 a)$$
Lean4
theorem eqOn_of_comp_eqOn (hs : IsPreconnected s) (h₁ : ContinuousOn g₁ s) (h₂ : ContinuousOn g₂ s)
(he : s.EqOn (p ∘ g₁) (p ∘ g₂)) {a : A} (has : a ∈ s) (ha : g₁ a = g₂ a) : s.EqOn g₁ g₂ :=
by
rw [← Set.restrict_eq_restrict_iff] at he ⊢
rw [continuousOn_iff_continuous_restrict] at h₁ h₂
rw [isPreconnected_iff_preconnectedSpace] at hs
exact sep.eq_of_comp_eq inj h₁ h₂ he ⟨a, has⟩ ha
