le_iInf₂_iff

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#le_iInf₂_iff

English

Same as le_iInf₂_iff, expressed as a simp-friendly form.

Русский

То же самое, выражено в виде простого правила симпа.

LaTeX

$$$\\\\left( a \\\\le iInf fun i => iInf fun j => f i j \\\\right) \\\\Leftrightarrow \\\\forall (i : ι) (j : κ i), a \\\\le f i j$$$

Lean4

theorem le_iInf₂_iff {f : ∀ i, κ i → α} : (a ≤ ⨅ (i) (j), f i j) ↔ ∀ i j, a ≤ f i j := by simp_rw [le_iInf_iff]

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

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

Разделы

Аффилиация

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