comp_continuousOn_iff — Mathlib

English

The map e ∘ f is continuous if and only if f is continuous (when e is a continuous linear equivalence).

Русский

Отображение e ∘ f непрерывно тогда и только тогда, когда f непрерывно (когда e — непрерывное линейное эквивалентное отображение).

LaTeX

$$$\text{Continuous}(e \circ f) \iff \text{Continuous}(f)$$$

Lean4

theorem comp_continuousOn_iff {α : Type*} [TopologicalSpace α] (e : M₁ ≃SL[σ₁₂] M₂) {f : α → M₁} {s : Set α} :
    ContinuousOn (e ∘ f) s ↔ ContinuousOn f s :=
  e.toHomeomorph.comp_continuousOn_iff _ _

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