units_iInf₂ — Mathlib

English

For a two-parameter indexed family, the units commute with the two-fold infimum: (iInf i) (iInf j) f i j .units equals iInf i (iInf j) (f i j).units.

Русский

Для двойной индексации единицы совпадают с двойной инфимумацией.

LaTeX

$$$ (iInf f).units = iInf_i (iInf_j (f(i,j)).units) $$$

Lean4

@[to_additive]
theorem units_iInf₂ {ι : Sort*} {κ : ι → Sort*} (f : (i : ι) → κ i → Submonoid M) :
    (⨅ (i : ι), ⨅ (j : κ i), f i j).units = ⨅ (i : ι), ⨅ (j : κ i), (f i j).units :=
  ofUnits_units_gc.u_iInf₂

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