le_iSup_iff

Mathlib.Order.CompleteLattice.Defs

URI: https://scilib.ai/kg/mathlib#le_iSup_iff

English

For any s : ι → α, a ≤ iSup s if and only if ∀ b, (∀ i, s i ≤ b) → a ≤ b.

Русский

Для любого s : ι → α, a ≤ iSup s тогда и только тогда, когда ∀ b, (∀ i, s i ≤ b) → a ≤ b.

LaTeX

$$$ a \le iSup s \iff \forall b, (\forall i, s i \le b) \rightarrow a \le b $$$

Lean4

theorem le_iSup_iff {s : ι → α} : a ≤ iSup s ↔ ∀ b, (∀ i, s i ≤ b) → a ≤ b := by simp [iSup, le_sSup_iff, upperBounds]

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

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

Разделы

Аффилиация

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