English
Let α, β be lattices with α complete, and f: α → β an antitone map. For any family s(i, j) ∈ α indexed by i and j, the supremum over i and j of f(s(i, j)) is bounded above by f of the infimum over i and j of s(i, j): ⨆i⨆j f(s(i, j)) ≤ f(⨅i⨅j s(i, j)).
Русский
Пусть α, β — полные решетки, f: α → β антимонотонна. Для семейства s(i, j) ∈ α верно неравенство: ⨆i⨆j f(s(i, j)) ≤ f(⨅i⨅j s(i, j)).
LaTeX
$$$\\\\big\\\\vee_{i}\\\\big\\\\vee_{j} f(s(i,j)) \\\\le f\\\\left(\\\\big\\\\wedge_{i}\\\\big\\\\wedge_{j} s(i,j)\\\\right)$$$
Lean4
theorem le_map_iInf₂ [CompleteLattice β] {f : α → β} (hf : Antitone f) (s : ∀ i, κ i → α) :
⨆ (i) (j), f (s i j) ≤ f (⨅ (i) (j), s i j) :=
hf.dual_left.le_map_iSup₂ _
