iSup_iInf_of_antitone — Mathlib

English

Dual formulation: swapping the order on the opposite order yields the same equality.

Русский

Дуальная формулировка: обмен порядка на противоположный даёт равенство.

LaTeX

$$$\text{finite}(\iota) \Rightarrow \text{Monotone}(f(i)) \Rightarrow \text{Eq}(\,iSup\; j\; iInf\; f(i,j),\ iInf\; i\; iSup\; j\; f(i,j)\).$$$

Lean4

theorem iSup_iInf_of_antitone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' (swap (· ≤ ·))]
    [Order.Frame α] {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_left

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