left_U_subset

Mathlib.Topology.UrysohnsLemma

URI: https://scilib.ai/kg/mathlib#Urysohns.CU.left_U_subset

English

The left U is contained in the original U of the CU data.

Русский

Левое U содержится в исходном U данных CU.

LaTeX

$$$c.left.U \\subseteq c.U$$$

Lean4

theorem left_U_subset (c : CU P) : c.left.U ⊆ c.U :=
  Subset.trans c.left_U_subset_right_C c.right.subset

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

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

Разделы

Аффилиация

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