forall_sigma_iff — Mathlib

English

A universal quantification over sigma is equivalent to a double universal quantification over i and a.

Русский

Универсальное кванторование над сигмой эквивалентно двойному по i и a.

LaTeX

$$$(\\forall x \\in S.\\sigma T, P x) \\iff (\\forall i \\in S, \\forall a \\in T(i), P(\\langle i,a\\rangle))$$$

Lean4

theorem forall_sigma_iff {p : (Σ i, α i) → Prop} : (∀ x ∈ s.sigma t, p x) ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃a⦄, a ∈ t i → p ⟨i, a⟩ :=
  by grind

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