iInf_iSup_of_antitone — Mathlib

English

Dual of the monotone case: for finite sets and Antitone f(i), the interchange equality holds in the opposite order.

Русский

Дуальная версия монотонного случая: для антимонотонного f(i) выполняется аналогичное равенство.

LaTeX

$$$\text{finite}(\iota) \Rightarrow \text{Eq}(\,iInf fun j => iSup fun i => f(i,j),\ iSup fun i => iInf fun j => f(i,j)).$$$

Lean4

theorem iInf_iSup_of_antitone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' (· ≤ ·)]
    [Order.Coframe α] {f : ι → ι' → α} (hf : ∀ i, Antitone (f i)) : ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j :=
  iSup_iInf_of_monotone (α := αᵒᵈ) fun i => (hf i).dual_right

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