const_of_comp — Mathlib

English

Let A be preconnected and g: A→E continuous. If f∘g is constant, then g is constant.

Русский

Пусть A предсоединённо и g: A→E непрерывно. Если f∘g постоянно, то g постоянно.

LaTeX

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

Lean4

theorem const_of_comp [PreconnectedSpace A] (cont : Continuous g) (he : ∀ a a', f (g a) = f (g a')) (a a') :
    g a = g a' :=
  hf.isSeparatedMap.const_of_comp hf.isLocalHomeomorph.isLocallyInjective cont he a a'

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