exists_prod_set — Mathlib

English

There exists x ∈ s × t such that p x if and only if there exist x ∈ s and y ∈ t such that p (x, y).

Русский

Существует x ∈ s × t такое, что p(x) тогда существует x ∈ s и y ∈ t такое, что p(x,y).

LaTeX

$$$ (\exists x \in s \times t, p x) \iff \exists x \in s, \exists y \in t, p (x, y) $$$

Lean4

theorem exists_prod_set {p : α × β → Prop} : (∃ x ∈ s ×ˢ t, p x) ↔ ∃ x ∈ s, ∃ y ∈ t, p (x, y) := by simp [and_assoc]

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