count_lt_count_succ_iff — Mathlib

English

For any p, count p (n+1) equals count p n plus 1 if p n holds; otherwise equals count p n, equivalently count p (n+1) = count p n + 1 iff p n.

Русский

Для любого p: count p (n+1) = count p n + 1 тогда и только тогда, когда p(n) истинно.

LaTeX

$$$$\operatorname{count}(p, n+1) = \operatorname{count}(p, n) + 1 \iff p(n).$$$$

Lean4

@[simp]
theorem count_lt_count_succ_iff {n : ℕ} : count p n < count p (n + 1) ↔ p n := by grind

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