continuousWithinAt — Mathlib

English

For any subset s of H and any x in H, the coordinate map I.toFun' is continuous within s at x.

Русский

Для любого подмножества s пространства H и любой точки x непрерывность координатной карты I.toFun' внутри s в точке x.

LaTeX

$$$ \\forall s \\; \\forall x:\\, \\text{ContinuousWithinAt}(I.toFun', s, x) $$$

Lean4

protected theorem continuousWithinAt {s x} : ContinuousWithinAt I s x :=
  I.continuousAt.continuousWithinAt

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