disjoint_C_support_lim

Mathlib.Topology.UrysohnsLemma

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

← MathLib Explorer

English

The C component and the support of lim are disjoint: Disjoint c.C (Function.support c.lim).

Русский

Компонента C и опорa lim дизъюнктны: Disjoint c.C (Function.support c.lim).

LaTeX

$$$Disjoint\\ c.C\\ (Function.support\\ c.lim)$$$

Lean4

theorem disjoint_C_support_lim (c : CU P) : Disjoint c.C (Function.support c.lim) :=
  Function.disjoint_support_iff.mpr (fun x hx => lim_of_mem_C c x hx)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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