iInf_psigma' — Mathlib

English

Let f : (i) → (κ i → α). Then iInf over i of iInf over j of f i j equals iInf over x : Σ i, κ i of f x.fst x.snd.

Русский

Пусть f : ∀ i, κ i → α. Тогда iInf по i и по j равен iInf по x : Σ i, κ i, f x.fst x.snd.

LaTeX

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

Lean4

theorem iInf_psigma' {ι : Sort*} {κ : ι → Sort*} (f : ∀ i, κ i → α) :
    (⨅ i, ⨅ j, f i j) = ⨅ ij : Σ' i, κ i, f ij.1 ij.2 :=
  (iInf_psigma fun x ↦ f x.1 x.2).symm

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