continuousAt_iff — Mathlib

English

If hg is IsInducing g, then ContinuousAt f x is equivalent to ContinuousAt (g ∘ f) x.

Русский

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

LaTeX

$$$\operatorname{IsInducing}(g) \Rightarrow \forall x, \big( \operatorname{ContinuousAt}(f, x) \iff \operatorname{ContinuousAt}(g \circ f, x) \big).$$$

Lean4

theorem continuousAt_iff (hg : IsInducing g) {x : X} : ContinuousAt f x ↔ ContinuousAt (g ∘ f) x :=
  hg.tendsto_nhds_iff

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