nth_zero_of_exists — Mathlib

English

If there exists x with p x, then nth p 0 equals Nat.find h where h: exists x, p x.

Русский

Если существует x с p x, тогда nth p 0 равен Nat.find h, где h: Exists x, p x.

LaTeX

$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ [DecidablePred p] \\\\ (\\\\exists n, p n)\\\\Rightarrow \\\\ nth\\\\ p\\\\ 0 =\\\\ Nat.find\\\\(\\\\exists\\\\ p).$$$

Lean4

theorem nth_zero_of_exists [DecidablePred p] (h : ∃ n, p n) : nth p 0 = Nat.find h := by rw [nth_zero];
  convert Nat.sInf_def h

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