iInf_iSup_eq — Mathlib

English

As in the iInf_iSup_eq' formula, but stated in the language of CompletelyDistribLattice.MinimalAxioms for general f with indexing by a function g: ∀ a, κ a → α.

Русский

Как и в формуле iInf_iSup_eq', но饰 в терминах CompletelyDistribLattice.MinimalAxioms для обобщенной функции f с индексированием.

LaTeX

$$$\\text{Given } f : \\forall a, \\kappa(a) \\to α, \\ \\bigl( \\inf_i \\sup_j f(i,j) \\bigr) = \\sup_g \\inf_i f(i, g(i)).$$$

Lean4

theorem iInf_iSup_eq [CompletelyDistribLattice α] {f : ∀ a, κ a → α} :
    (⨅ a, ⨆ b, f a b) = ⨆ g : ∀ a, κ a, ⨅ a, f a (g a) :=
  CompletelyDistribLattice.MinimalAxioms.of.iInf_iSup_eq' _

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