ωSup_le_iff

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.ωSup_le_iff

← MathLib Explorer

English

ωSup c ≤ x is equivalent to c i ≤ x for all i.

Русский

ωSup c ≤ x эквивалентно c(i) ≤ x для всех i.

LaTeX

$$$$ \omegaSup c \le x \quad\Longleftrightarrow\quad \forall i,\ c(i) \le x. $$$$

Lean4

@[simp]
theorem ωSup_le_iff {c : Chain α} {x : α} : ωSup c ≤ x ↔ ∀ i, c i ≤ x :=
  by
  constructor <;> intros
  · trans ωSup c
    · exact le_ωSup _ _
    · assumption
  exact ωSup_le _ _ ‹_›

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

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

Разделы

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

Аффилиация

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