iInf_iSup_of_monotone — Mathlib

English

For finite index sets and f(i) monotone, the interchange of iInf and iSup holds: ⨅ j ⨆ i f(i,j) = ⨆ i ⨅ j f(i,j).

Русский

Для конечного множества индексов и монотонного f(i): обмен iInf и iSup сохраняет равенство.

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_monotone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' (swap (· ≤ ·))]
    [Order.Coframe α] {f : ι → ι' → α} (hf : ∀ i, Monotone (f i)) : ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j :=
  iSup_iInf_of_antitone (α := αᵒᵈ) fun i => (hf i).dual_right

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