forall — Mathlib

English

A property holds for all elements of M/p iff it holds for all representatives in M.

Русский

Свойство верно для всех элементов M/p тогда и только тогда, когда верно для всех представителей в M.

LaTeX

$$$(\forall a: M/p, P(a)) \iff (\forall x\in M, P(\operatorname{mk}(x))).$$$

Lean4

protected nonrec theorem «forall» {P : M ⧸ p → Prop} : (∀ a, P a) ↔ ∀ a, P (mk a) :=
  Quotient.forall

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