iInf₂_sup_eq — Mathlib

English

For a family f : ∀ i, κ i → α, the infimum over i and j of f(i,j) joined with a equals the infimum over i,j of a ⊔ f(i,j).

Русский

Для семейства f(i,j) инфимума по i и j с верхним пределом a равно инфимуму по i,j от (a ⊔ f(i,j)).

LaTeX

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

Lean4

theorem iInf₂_sup_eq {f : ∀ i, κ i → α} (a : α) : (⨅ (i) (j), f i j) ⊔ a = ⨅ (i) (j), f i j ⊔ a :=
  @iSup₂_inf_eq αᵒᵈ _ _ _ _ _

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