subtype

Mathlib.Topology.Metrizable.Basic

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.MetrizableSpace.subtype

English

If X is metrizable, then any subtype s ⊆ X is metrizable.

Русский

Если X метризуемо, то любой подпредмет s ⊆ X метризуем.

LaTeX

$$$[\text{MetrizableSpace } X] \Rightarrow [\text{MetrizableSpace } s]$$$

Lean4

instance subtype [MetrizableSpace X] (s : Set X) : MetrizableSpace s :=
  IsEmbedding.subtypeVal.metrizableSpace

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

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

Разделы

Аффилиация

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