comp_continuous_iff — Mathlib

English

The composite with e is continuous iff the inner function is continuous, in a variant with Homeomorph.

Русский

Сочетание с e непрерывно тогда и только тогда, когда внутренняя функция непрерывна (вариант с Homeomorph).

LaTeX

$$$ Continuous (e \circ f) \iff Continuous f $$$

Lean4

theorem comp_continuous_iff {α : Type*} [TopologicalSpace α] (e : A ≃A[R] B) {f : α → A} :
    Continuous (e ∘ f) ↔ Continuous f :=
  e.toHomeomorph.comp_continuous_iff

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