constOn_of_comp — Mathlib

English

Let A be preconnected and cont : Continuous g. If ∀ a,a' ∈ A, f(g(a)) = f(g(a')), then g(a) = g(a') for all a,a'.

Русский

Пусть A предсоединённо, g:A→E непрерывно. Если для всех a,a' ∈ A выполняется f(g(a))=f(g(a')), то g(a)=g(a') для любых a,a'.

LaTeX

$$$[\text{Preconnected}(A)]\ (\text{Continuous}(g))\ \bigl(\forall a,a',\ f(g(a))=f(g(a'))\bigr)\Rightarrow g(a)=g(a').$$$

Lean4

theorem constOn_of_comp (hs : IsPreconnected s) (cont : ContinuousOn g s) (he : ∀ a ∈ s, ∀ a' ∈ s, f (g a) = f (g a'))
    {a a'} (ha : a ∈ s) (ha' : a' ∈ s) : g a = g a' :=
  hf.isSeparatedMap.constOn_of_comp hf.isLocalHomeomorph.isLocallyInjective hs cont he ha ha'

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