forall — Mathlib

English

For any predicate P on SeparationQuotient(X), existence of a witness is equivalent to the existence of a witness in X via mk.

Русский

Для любого предиката P на SeparationQuotient(X) существование доказательства эквивалентно существованию доказательства в X через mk.

LaTeX

$$$\\exists x: \\mathrm{SeparationQuotient}(X), P(x) \\iff \\exists x: X, P(\\mathrm{mk}(x)).$$$

Lean4

protected theorem «forall» {P : SeparationQuotient X → Prop} : (∀ x, P x) ↔ ∀ x, P (.mk x) :=
  Quotient.forall

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