forall_prod_set — Mathlib

English

Let p be a predicate on α × β. Then (for all x ∈ s × t, p x) holds if and only if (for all x ∈ s, for all y ∈ t, p (x, y)).

Русский

Пусть p — предикат на α × β. Тогда (для всех x ∈ s × t, p(x)) эквивалентно (для всех x ∈ s и для всех y ∈ t, p(x,y)).

LaTeX

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

Lean4

theorem forall_prod_set {p : α × β → Prop} : (∀ x ∈ s ×ˢ t, p x) ↔ ∀ x ∈ s, ∀ y ∈ t, p (x, y) :=
  prod_subset_iff

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