exists_sigma_iff — Mathlib

English

There exists an element in a sigma such that a property holds is equivalent to the existence of i ∈ s and a ∈ t i with the property.

Русский

Существование элемента в сигме с свойством эквивалентно существованию i∈s и a∈t i с этим свойством.

LaTeX

$$$(\\exists x \\in s.\\sigma t, P x) \\iff \\exists i \\in s, \\exists a \\in t(i), P(\\langle i,a\\rangle)$$$

Lean4

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

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