subset_right_C

Mathlib.Topology.UrysohnsLemma

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

English

The C component of a CU is contained in the C component of its right variant.

Русский

Компонента C из CU содержится в C правого варианта.

LaTeX

$$$c.C \\subseteq c.right.C$$$

Lean4

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

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

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

Разделы

Аффилиация

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