forall_ne_zero_iff — Mathlib

English

For any predicate P on natural numbers, (for all i ≠ 0, P i) is equivalent to (for all i, P(i+1)).

Русский

Для любого свойства P над натуральными числами эквивалентно: для всех i ≠ 0 выполняется P i тогда и только тогда, когда для всех i выполняется P(i+1).

LaTeX

$$$\\\\forall P:\\\\mathbb N \\\\to \\\\text{Prop}, \\\\left(\\\\forall i \\\\in \\\\mathbb N, i \\\\neq 0 \\\\Rightarrow P(i)\\\\right) \\\\iff \\\\left(\\\\forall i \\\\in \\\\mathbb N, P(i+1)\\\\right).$$$

Lean4

theorem forall_ne_zero_iff (P : ℕ → Prop) : (∀ i, i ≠ 0 → P i) ↔ (∀ i, P (i + 1)) :=
  SuccOrder.forall_ne_bot_iff P

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