chainSupCarrier

Mathlib.Topology.ShrinkingLemma

URI: https://scilib.ai/kg/mathlib#ShrinkingLemma.PartialRefinement.chainSupCarrier

← MathLib Explorer

English

If v is in a chain c, then v ≤ chainSup c, i.e., v is below the supremum of the chain.

Русский

Если v входит в цепь c, тогда v ниже верхней грани chainSup c.

LaTeX

$$v ≤ chainSup c hc ne hfin hU$$

Lean4

/-- The carrier of the least upper bound of a non-empty chain of partial refinements is the union of
their carriers. -/
def chainSupCarrier (c : Set (PartialRefinement u s p)) : Set ι :=
  ⋃ v ∈ c, carrier v

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

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

Разделы

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

Аффилиация

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