exists_upper_bound

Mathlib.FieldTheory.Extension

URI: https://scilib.ai/kg/mathlib#IntermediateField.Lifts.exists_upper_bound

← MathLib Explorer

English

A chain of lifts has an upper bound in the directed order.

Русский

Цепь Lift имеет верхнюю границу в направленном порядке.

LaTeX

$$$\exists ub, \forall a \in c, a \le ub$$$

Lean4

/-- A chain of lifts has an upper bound. -/
theorem exists_upper_bound (c : Set (Lifts F E K)) (hc : IsChain (· ≤ ·) c) : ∃ ub, ∀ a ∈ c, a ≤ ub :=
  ⟨_, le_union c hc⟩

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

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

Разделы

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

Аффилиация

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