comp_continuousOn_iff — Mathlib

English

Similar to the previous, for γ with a topological structure: ContinuousOn ((f) ∘ g) s ↔ ContinuousOn g s.

Русский

Аналогично предыдущему, для произвольного γ с топологической структурой: ContinuousOn((f)∘g) s эквивалентно ContinuousOn g s.

LaTeX

$$$\\text{ContinuousOn}((f : \\alpha \\to \\beta) \\circ g)\\; s \\iff \\text{ContinuousOn}\\; g\\; s$$$

Lean4

theorem comp_continuousOn_iff {γ} [TopologicalSpace γ] {g : γ → α} {s : Set γ} :
    ContinuousOn ((f : α → β) ∘ g) s ↔ ContinuousOn g s :=
  (Dilation.isUniformInducing f).isInducing.continuousOn_iff.symm

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