iSup_inf_eq — Mathlib

English

In a CompletelyDistribLattice, for any f : ∀ a, κ a → α, the iInf_iSup_eq' identity holds: ⨅ a, ⨆ b, f a b = ⨆ g : ∀ a, κ a, ⨅ a, f a (g a).

Русский

В полной распределимой решетке верно: ⨅a ⨆b f(a,b) = ⨆g ⨅a f(a,g(a)).

LaTeX

$$$\\inf_{a} \\sup_{b} f(a,b) = \\sup_{g} \\inf_{a} f(a, g(a))$$$

Lean4

theorem iSup_inf_eq (f : ι → α) (a : α) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a := by rw [iSup, sSup_inf_eq, iSup_range]

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