comp_continuous_iff — Mathlib

English

If h: X ≃ₜ Y is a homeomorphism, then for any f: Z → X, the composition h ∘ f is continuous iff f is continuous.

Русский

Если h: X ≃ₜ Y — гомеоморфизм, то для любого f: Z → X композиция h ∘ f непрерывна тогда и только тогда, когда f непрерывна.

LaTeX

$$$Continuous(h \circ f) \iff Continuous(f).$$$

Lean4

@[simp]
theorem comp_continuous_iff (h : X ≃ₜ Y) {f : Z → X} : Continuous (h ∘ f) ↔ Continuous f :=
  h.isInducing.continuous_iff.symm

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