nth_true — Mathlib

English

Let p: ℕ → Prop be such that p(n) holds for all n. Then nth p n = n.

Русский

Пусть p : ℕ → Prop тождественно истинно; тогда для каждого n выполняется nth p n = n.

LaTeX

$$$$ \forall p:\mathbb{N}\to \mathsf{Prop}, \big(\forall m:\mathbb{N}, p(m)\big) \rightarrow \forall n:\mathbb{N}, \operatorname{nth} p n = n. $$$$

Lean4

@[simp]
theorem nth_true (n : ℕ) : nth (fun _ ↦ True) n = n :=
  nth_of_forall fun _ _ ↦ trivial

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