continuousAt_iff' — Mathlib

English

If hf is IsInducing f and range f ∈ 𝓝(f x), then ContinuousAt (g ∘ f) x ⇔ ContinuousAt g (f x).

Русский

Если hf — IsInducing f и range f ∈ 𝓝(f x), то ContinuousAt (g ∘ f) x эквивалено ContinuousAt g (f x).

LaTeX

$$$\operatorname{IsInducing}(f) \Rightarrow \forall x, \left( \operatorname{range}(f) \in \mathcal{N}(f(x)) \Rightarrow \big( \operatorname{ContinuousAt}(g \circ f, x) \iff \operatorname{ContinuousAt}(g, f(x)) \big) \right).$$$

Lean4

theorem continuousAt_iff' (hf : IsInducing f) {x : X} (h : range f ∈ 𝓝 (f x)) :
    ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x) := by
  simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]

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