forall — Mathlib

English

For every p : αᵒᵈ → Prop, (for all a, p a) is equivalent to (for all a, p (toDual a)).

Русский

Для любого p : αᵒᵈ → Prop верно: (для всех a, p a) эквивалентно (для всех a, p (toDual a)).

LaTeX

$$$\forall p:\alpha^{\mathrm{op}} \to \mathrm{Prop},\quad (\forall a, p\,a) \iff \forall a, p(\mathrm{toDual}\,a)$$$

Lean4

@[simp]
protected theorem «forall» {p : αᵒᵈ → Prop} : (∀ a, p a) ↔ ∀ a, p (toDual a) :=
  Iff.rfl

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