iSup_iInf_le — Mathlib

English

In a CompleteLattice, a specific inequality holds between iSup and iInf of a family of elements f a b.

Русский

В полной решётке выполняется неравенство между iSup и iInf семейства элементов f(a,b).

LaTeX

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

Lean4

theorem iSup_iInf_le [CompleteLattice α] {f : ∀ a, κ a → α} : ⨆ a, ⨅ b, f a b ≤ ⨅ g : ∀ a, κ a, ⨆ a, f a (g a) :=
  le_iInf_iSup (α := αᵒᵈ)

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