iSup₂_inf_eq — Mathlib

English

For a two-parameter family f : ∀ i, κ i → α and an element a, the two-index iSup often commutes with infimum: (⨆ i (j), f i j) ⊓ a = ⨆ i (j), f i j ⊓ a.

Русский

Для двойного индекса f(i,j) выполняется обмен инф и суп: (⨆ i j f(i,j)) ∧ a = ⨆ i j (f(i,j) ∧ a).

LaTeX

$$$\\bigl( \\bigvee_{i,j} f(i,j) \\bigr) \\wedge a = \\bigvee_{i,j} (f(i,j) \\wedge a)$$$

Lean4

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

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