comp_continuous_iff — Mathlib

English

Continuous of the composition equals continuous of the inner function when composed with a dilation.

Русский

Непрерывность композиции равна непрерывности внутренней функции при композиции с дилатацией.

LaTeX

$$$\\text{Continuous}((f : \\alpha \\to \\beta) \\circ g) \\iff \\text{Continuous} g$$$

Lean4

theorem comp_continuous_iff {γ} [TopologicalSpace γ] {g : γ → α} : Continuous ((f : α → β) ∘ g) ↔ Continuous g :=
  (Dilation.isUniformInducing f).isInducing.continuous_iff.symm

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