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