continuousAt_subtype_val

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#continuousAt_subtype_val

English

The projection from a subtype to the ambient space is continuous at every point.

Русский

Проекция из подтипа в окружающее пространство непрерывна в любой точке.

LaTeX

$$$\text{ContinuousAt}(\text{Subtype.val})\;\text{ at any } x.$$$

Lean4

theorem continuousAt_subtype_val {p : X → Prop} {x : Subtype p} : ContinuousAt ((↑) : Subtype p → X) x :=
  continuous_subtype_val.continuousAt

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

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

Разделы

Аффилиация

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