continuousWithinAt_iff — Mathlib

English

If g is an inducing map, then continuity within at a is preserved by composition with g: ContinuousWithinAt f s x iff ContinuousWithinAt (g ∘ f) s x.

Русский

Если g есть индуциирующая отображение, то непрерывность внутри в точке сохраняется при композиции: ContinuousWithinAt f s x эквивалентно ContinuousWithinAt (g ∘ f) s x.

LaTeX

$$$\\text{IsInducing } g \\Rightarrow (\\text{ContinuousWithinAt } f\\ s\\ x) \\iff (\\text{ContinuousWithinAt } (g \\circ f)\\ s\\ x)$$$

Lean4

theorem continuousWithinAt_iff {f : α → β} {g : β → γ} (hg : IsInducing g) {s : Set α} {x : α} :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x := by simp_rw [ContinuousWithinAt, hg.tendsto_nhds_iff];
  rfl

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