English
For a four-argument function f, the quadruple supremum can be reordered: ⨆ i1 j1 i2 j2 f(i1,j1,i2,j2) equals ⨆ i2 j2 i1 j1 f(i1,j1,i2,j2).
Русский
Для функции четырёх аргументов f допускается перестановка локальных индексов в четырёхкратном супремуме.
LaTeX
$$$$\bigvee_{i_1} \bigvee_{j_1} \bigvee_{i_2} \bigvee_{j_2} f(i_1,j_1,i_2,j_2) = \bigvee_{i_2} \bigvee_{j_2} \bigvee_{i_1} \bigvee_{j_1} f(i_1,j_1,i_2,j_2).$$$$
Lean4
theorem iSup₂_comm {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} (f : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → α) :
⨆ (i₁) (j₁) (i₂) (j₂), f i₁ j₁ i₂ j₂ = ⨆ (i₂) (j₂) (i₁) (j₁), f i₁ j₁ i₂ j₂ := by
simp only [@iSup_comm _ (κ₁ _), @iSup_comm _ ι₁]
