English
If p: ℕ → Prop is false for every n' ≥ n, then nth p n = 0.
Русский
Если для всех n' ≥ n выполняется ¬p(n'), то n-й элемент последовательности, задаваемой p, равен 0.
LaTeX
$$$$ \forall p:\mathbb{N}\to \mathsf{Prop}, \forall n:\mathbb{N}, \Big(\forall n':\mathbb{N}, n' \ge n \rightarrow \neg p(n')\Big) \rightarrow \operatorname{nth} p n = 0. $$$$
Lean4
theorem nth_of_forall_not {n : ℕ} (hp : ∀ n' ≥ n, ¬p n') : nth p n = 0 :=
by
have : setOf p ⊆ Finset.range n := by
intro n' hn'
contrapose! hp
exact ⟨n', by simpa using hp, Set.mem_setOf.mp hn'⟩
rw [nth_of_card_le ((finite_toSet _).subset this)]
· refine (Finset.card_le_card ?_).trans_eq (Finset.card_range n)
exact Set.Finite.toFinset_subset.mpr this
