uniformContinuous_comap' — Mathlib

English

If UniformContinuous (f ∘ g) then g is UniformContinuous from α to γ with target (UniformSpace.comap f v).

Русский

Если UniformContinuous (f ∘ g), то отображение g: α → γ равно UniformContinuous при целевом пространстве γ, на которое действует comap f v.

LaTeX

$$UniformContinuous (f ∘ g) ⇒ UniformContinuous g$$

Lean4

theorem uniformContinuous_comap' {f : γ → β} {g : α → γ} [v : UniformSpace β] [u : UniformSpace α]
    (h : UniformContinuous (f ∘ g)) : @UniformContinuous α γ u (UniformSpace.comap f v) g :=
  tendsto_comap_iff.2 h

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