comp_continuousAt_iff' — Mathlib

English

For a homeomorphism h: X ≃ₜ Y and a function f: Y → Z, ContinuousAt (f ∘ h) x ↔ ContinuousAt f (h x) for x ∈ X.

Русский

Для гомеоморфизма h: X ≃ₜ Y и функции f: Y → Z выполняется ContinuousAt (f ∘ h) x ↔ ContinuousAt f (h x) при x ∈ X.

LaTeX

$$$ContinuousAt(f \circ h, x) \iff ContinuousAt(f, h(x)).$$$

Lean4

theorem comp_continuousAt_iff' (h : X ≃ₜ Y) (f : Y → Z) (x : X) : ContinuousAt (f ∘ h) x ↔ ContinuousAt f (h x) :=
  h.isInducing.continuousAt_iff' (by simp)

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