iInf_psigma — Mathlib

English

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

Русский

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

LaTeX

$$$$ \iInf_{ij} f_{ij} = \iInf_{x : \Sigma i, κ i} f x.1 x.2 $$$$

Lean4

theorem iInf_psigma {ι : Sort*} {κ : ι → Sort*} (f : (Σ' i, κ i) → α) : ⨅ ij, f ij = ⨅ i, ⨅ j, f ⟨i, j⟩ :=
  eq_of_forall_le_iff fun c ↦ by simp only [le_iInf_iff, PSigma.forall]

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