forall — Mathlib

English

A predicate on Colex α holds for all elements of Colex α iff it holds for all toColex-images of elements of α.

Русский

Любое свойство на Colex α выполняется для всех элементов Colex α тогда и только тогда, когда оно выполняется для всех изображений toColex от элементов α.

LaTeX

$$$\\forall p:\\\\ Colex\\,α \\to \\text{Prop},\\; (\\forall a:\\\\ Colex\\,α,\\; p(a)) \\\\iff (\\forall a:\\\\ α,\\; p(toColex\\,a))$$$

Lean4

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

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