forall_iff — Mathlib

English

Let p be a predicate on DegLex α. Then p holds for every DegLex element if and only if p holds on all elements of the form toDegLex(a) as a runs over α.

Русский

Пусть p — предикат на DegLex α. Тогда p выполняется для всех элементов DegLex тогда и только тогда, когда p выполняется для всех элементов вида toDegLex(a), где a пробегает по α.

LaTeX

$$$(\forall x:\DegLex(\alpha),\ p(x)) \iff (\forall a:\alpha,\ p(toDegLex(a)))$$$

Lean4

@[simp]
theorem forall_iff {p : DegLex α → Prop} : (∀ a, p a) ↔ ∀ a, p (toDegLex a) :=
  Iff.rfl

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