forall — Mathlib

English

For every property p on NN Rat, (∀ q, p q) is equivalent to (∀ q hq, p ⟨q, hq⟩).

Русский

Для каждого свойства p над NN Rat выполняется эквивалентность: (∀ q, p q) ⇔ ∀ q hq, p ⟨q, hq⟩.

LaTeX

$$$\forall p : \mathbb{Q}_{\ge 0} \to \mathrm{Prop},\ (\forall q, p q) \iff \forall q hq, p \langle q,hq \rangle$$$

Lean4

theorem «forall» {p : ℚ≥0 → Prop} : (∀ q, p q) ↔ ∀ q hq, p ⟨q, hq⟩ :=
  Subtype.forall

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