left_U_subset_right_C

Mathlib.Topology.UrysohnsLemma

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

English

In the CU construction, the chosen left U is contained in the right C.

Русский

В конструкции CU выбранное множество U слева содержится в правом C.

LaTeX

$$$c.left.U \\subseteq c.right.C$$$

Lean4

theorem left_U_subset_right_C (c : CU P) : c.left.U ⊆ c.right.C :=
  subset_closure

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

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

Разделы

Аффилиация

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