le_iInf_iSup — Mathlib

English

In a CompleteLattice, an inequality relating iInf and iSup holds: ⨆ a, ⨅ b, f a b ≤ ⨅ g, ⨆ a, f a (g a).

Русский

В замкнутой (полной) решётке выполняется неравенство, связывающее iInf и iSup: ⨆ a, ⨅ b, f a b ≤ ⨅ g, ⨆ a, f a (g a).

LaTeX

$$$\big\vee_{a} \big\wedge_{b} f(a,b) \le \big\wedge_{g} \big\vee_{a} f(a,g(a))$$$

Lean4

theorem le_iInf_iSup [CompleteLattice α] {f : ∀ a, κ a → α} : (⨆ g : ∀ a, κ a, ⨅ a, f a (g a)) ≤ ⨅ a, ⨆ b, f a b :=
  iSup_le fun _ => le_iInf fun a => le_trans (iInf_le _ a) (le_iSup _ _)

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