subtype_val

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#Continuous.subtype_val

English

If f: Y → Subtype p is continuous, then the composition of f with Subtype.val is continuous.

Русский

Если f: Y → Subtype p непрерывно, то композиция f и Subtype.val непрерывна.

LaTeX

$$$$ \\text{Continuous}(f) \\Rightarrow \\text{Continuous}(\\lambda x. (f x).val). $$$$

Lean4

theorem subtype_val {f : Y → Subtype p} (hf : Continuous f) : Continuous fun x => (f x : X) :=
  continuous_subtype_val.comp hf

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

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

Разделы

Аффилиация

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