forall — Mathlib

English

A predicate p on ℂ is true for all z ∈ ℂ if and only if p is true for all pairs (a,b) ∈ ℝ × ℝ, where z = a + bi.

Русский

Утверждение p на ℂ истинно для всех z тогда и только тогда, когда p истинно для всех пар (a,b) в ℝ × ℝ, где z = a + bi.

LaTeX

$$$$ (\forall z \in \mathbb{C}, p(z)) \iff (\forall a,b \in \mathbb{R}, p(a + b i)). $$$$

Lean4

theorem «forall» {p : ℂ → Prop} : (∀ x, p x) ↔ ∀ a b, p ⟨a, b⟩ := by aesop

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