subtypeVal

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#Topology.IsInducing.subtypeVal

English

For any subset t ⊆ Y, the inclusion map i: t → Y is an inducing map.

Русский

Для любого подмножества t ⊆ Y включение i: t → Y является отображением, индуцирующим топологию.

LaTeX

$$$$ \\text{IsInducing}((\\uparrow):t\\to Y). $$$$

Lean4

theorem subtypeVal {t : Set Y} : IsInducing ((↑) : t → Y) :=
  ⟨rfl⟩

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

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

Разделы

Аффилиация

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