sup_iInf₂_eq — Mathlib

English

For a family f : ∀ i, κ i → α and an element a, a ⊔ ⨅ i (⨅ j, f(i,j)) equals ⨅ i (⨅ j, a ⊔ f(i,j)).

Русский

Для семейства f(i,j) и элемента a: a ⊔ ⨅_{i,j} f(i,j) = ⨅_i, ⨅_j, a ⊔ f(i,j).

LaTeX

$$$a \vee \bigwedge_{i} \bigwedge_{j} f(i,j) = \bigwedge_{i} \bigwedge_{j} (a \vee f(i,j))$$$

Lean4

theorem sup_iInf₂_eq {f : ∀ i, κ i → α} (a : α) : (a ⊔ ⨅ (i) (j), f i j) = ⨅ (i) (j), a ⊔ f i j :=
  @inf_iSup₂_eq αᵒᵈ _ _ _ _ _

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