forall — Mathlib

English

For any predicate p on α^{op}, (∀ a, p(a)) is equivalent to ∀ a: α, p(op a).

Русский

Для любого предиката p на α^{op} выполняется эквивалентность: (∧a, p(a)) эквивалентно ∀ a∈α, p(op(a)).

LaTeX

$$$\\\\forall a:\\\\alpha^{\\\\mathrm{op}}, \\\\; p(a) \\\\iff \\\\forall a:\\\\alpha, \\\\; p(\\\\mathrm{op}(a))$$$

Lean4

@[to_additive (attr := simp)]
theorem «forall» {p : αᵐᵒᵖ → Prop} : (∀ a, p a) ↔ ∀ a, p (op a) :=
  op_surjective.forall

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