English
The equation nth p n = 0 is equivalent to either p 0 and n = 0, or there exists a finite hf with #hf.toFinset ≤ n.
Русский
Равенство nth p n = 0 эквивалентно либо p 0 и n = 0, либо существует конечноe hf такое, что #hf.toFinset ≤ n.
LaTeX
$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ {n}:\\\\mathbb{N},\\\\ Eq\\\\(\\\\mathrm{nth}\\\\ p\\\\ n\\\\,\\\\ 0) \\\\Leftrightarrow \\\\Big(\\\\mathsf{Or}\\\\(\\\\wedge\\\\ p\\\\ 0\\\\ (n=0)) \\\\ (\\\\Exists hf:\\\\{x:\\\\mathbb{N}\\\\mid p x\\\\}\\\\Finite,\\\\ #hf.toFinset \\\\le n)\\\\Big).$$$
Lean4
theorem nth_eq_zero {n} : nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ hf : (setOf p).Finite, #hf.toFinset ≤ n :=
by
refine ⟨fun h => ?_, ?_⟩
· simp only [or_iff_not_imp_right, not_exists, not_le]
exact fun hn => ⟨h ▸ nth_mem _ hn, nonpos_iff_eq_zero.1 <| h ▸ le_nth hn⟩
· rintro (⟨h₀, rfl⟩ | ⟨hf, hle⟩)
exacts [nth_zero_of_zero h₀, nth_of_card_le hf hle]
