English
For a two-parameter indexed function f, the quadruple infimum can be swapped: ⨅ i1 j1 i2 j2 f(i1,j1,i2,j2) equals ⨅ i2 j2 i1 j1 f(i1,j1,i2,j2).
Русский
Для функции с двумя параметрами инфимум можно переставлять пары индексов.
LaTeX
$$$$\bigwedge_{i_1} \bigwedge_{j_1} \bigwedge_{i_2} \bigwedge_{j_2} f(i_1,j_1,i_2,j_2) = \bigwedge_{i_2} \bigwedge_{j_2} \bigwedge_{i_1} \bigwedge_{j_1} f(i_1,j_1,i_2,j_2).$$$$
Lean4
theorem iInf₂_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 [@iInf_comm _ (κ₁ _), @iInf_comm _ ι₁]
/- TODO: this is strange. In the proof below, we get exactly the desired among the equalities,
but close does not get it.
begin
apply @le_antisymm,
simp, intros,
begin [smt]
ematch, ematch, ematch, trace_state, have := le_refl (f i_1 i),
trace_state, close
end
end
-/
