comp_continuousAt_iff — Mathlib

English

If h: X ≃ₜ Y is a homeomorphism, then for a function f: Z → X and a point z ∈ Z, ContinuousAt (h ∘ f) z ↔ ContinuousAt f z.

Русский

Если h: X ≃ₜ Y — гомеоморфизм, то для функции f: Z → X и точки z ∈ Z выполняется ContinuousAt (h ∘ f) z ↔ ContinuousAt f z.

LaTeX

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

Lean4

theorem comp_continuousAt_iff (h : X ≃ₜ Y) (f : Z → X) (z : Z) : ContinuousAt (h ∘ f) z ↔ ContinuousAt f z :=
  h.isInducing.continuousAt_iff.symm

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