constOn_of_comp — Mathlib

English

If p is separated and locally injective, and two lifts g a constant under p, then g(a) is independent of a.

Русский

Если p разделяющее и локально инъективное, и g константна по композиции, то g однозначна.

LaTeX

$$IsSeparatedMap p → IsLocallyInjective p → ∀ a a', p (g a) = p (g a') → g a = g a'$$

Lean4

theorem constOn_of_comp (hs : IsPreconnected s) (cont : ContinuousOn g s) (he : ∀ a ∈ s, ∀ a' ∈ s, p (g a) = p (g a'))
    {a a'} (ha : a ∈ s) (ha' : a' ∈ s) : g a = g a' :=
  sep.eqOn_of_comp_eqOn inj hs cont continuous_const.continuousOn (fun a ha ↦ he a ha a' ha') ha' rfl ha

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