iInf_sigma' — Mathlib

English

Let f : Σ p → α. Then iInf over i, j of f i j equals iInf over x : Σ i, κ i of f x.1 x.2.

Русский

Пусть f : Σ p → α. Тогда iInf по i, j равен iInf по x : Σ i, κ i, f x.1 x.2.

LaTeX

$$$$ \iInf_{i} \iInf_{j} f i j = \iInf_{x : \Sigma i, \kappa i} f x.1 x.2 $$$$

Lean4

theorem iInf_sigma' {κ : β → Type*} (f : ∀ i, κ i → α) : (⨅ i, ⨅ j, f i j) = ⨅ x : Σ i, κ i, f x.1 x.2 :=
  (iInf_sigma (f := fun x ↦ f x.1 x.2)).symm

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