continuousWithinAt

Mathlib.Analysis.Normed.Affine.Isometry

URI: https://scilib.ai/kg/mathlib#AffineIsometryEquiv.continuousWithinAt

English

A affine isometry is continuous within any set at a point.

Русский

Афинная изометрия непрерывна внутри любых множеств в точке.

LaTeX

$$$\\forall s x, \\text{ContinuousWithinAt}(e, s, x)$$$

Lean4

protected theorem continuousWithinAt {s x} : ContinuousWithinAt e s x :=
  e.continuous.continuousWithinAt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru