forall — Mathlib

English

The forall lemma asserts that a property holds for all archimedean classes iff it holds for all representatives, i.e., ∀ A, p A ↔ ∀ a, p mk a.

Русский

Лемма forall утверждает, что свойство выполняется для всех архимедовых классов тогда и только тогда, когда оно выполняется для всех представителей, то есть ∀ A, p A ↔ ∀ a, p (mk a).

LaTeX

$$$\forall A: MulArchimedeanClass M, P(A) \iff \forall a: M, P(mk(a))$$$

Lean4

@[to_additive]
theorem «forall» {p : MulArchimedeanClass M → Prop} : (∀ A, p A) ↔ ∀ a, p (mk a) :=
  Quotient.forall

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