sup_iInf₂_eq — Mathlib

English

For a family f : ∀ i, κ i → α and any a ∈ α, the two-step supremum with a distributes over the two-variable infimum: a ⊔ ⨅ i ⨅ j f(i,j) = ⨅ i ⨅ j (a ⊔ f(i,j)).

Русский

Пусть f(i,j) задано; тогда a ⊔ ⨅ i,j f(i,j) = ⨅ i,j (a ⊔ f(i,j)).

LaTeX

$$$ a \\lor \\inf_{i} \\inf_{j} f(i,j) = \\inf_{i} \\inf_{j} (a \\lor f(i,j)) $$$

Lean4

theorem sup_iInf₂_eq {f : ∀ i, κ i → α} (a : α) : (a ⊔ ⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, a ⊔ f i j := by
  simp only [sup_iInf_eq]

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