continuousOn_image_iff — Mathlib

English

If g is an inducing map, then a function g satisfies continuousOn on image f s iff f ∘ g is continuous on s.

Русский

Если g индуциирующее отображение, тогда для всякой s непрерывность на образе f s эквивалентна непрерывности f ∘ g на s.

LaTeX

$$$\\text{IsInducing } f \\Rightarrow (\\text{ContinuousOn } g (f''s) \\iff \\text{ContinuousOn } (g \\circ f) s)$$$

Lean4

theorem continuousOn_image_iff {g : β → γ} {s : Set α} (hf : IsInducing f) :
    ContinuousOn g (f '' s) ↔ ContinuousOn (g ∘ f) s := by
  simp [ContinuousOn, ContinuousWithinAt, ← hf.map_nhdsWithin_eq]

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