inf_iSup₂_eq — Mathlib

English

A two-dimensional refinement of inf-sup equality: infimum with a double supremum distributes into a double supremum of infima.

Русский

Улучшенная двумерная версия равенства инфимума и супремума: инфимум с двойным супремумом распределяется в двойной инфимум от элемента a и f(i,j).

LaTeX

$$$\min(a, \sup_i \sup_j f(i,j)) = \sup_i \sup_j \min(a, f(i,j))$$$

Lean4

theorem inf_iSup₂_eq {f : ∀ i, κ i → α} (a : α) : (a ⊓ ⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, a ⊓ f i j := by
  simp only [inf_iSup_eq]

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