continuousAt_coe — Mathlib

English

Continuity at a base point x ∈ X is equivalent to continuity of the composed map f ∘ ι at x.

Русский

Непрерывность в точке x ∈ X эквивалентна непрерывности композиции f ∘ ι в x.

LaTeX

$$$\text{ContinuousAt } f x \iff \text{ContinuousAt } (f \circ (\uparrow)) x$$$

Lean4

theorem continuousAt_coe {Y : Type*} [TopologicalSpace Y] {f : OnePoint X → Y} {x : X} :
    ContinuousAt f x ↔ ContinuousAt (f ∘ (↑)) x := by rw [ContinuousAt, nhds_coe_eq, tendsto_map'_iff, ContinuousAt];
  rfl

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