lt_card_toFinset_of_nth_ne_zero — Mathlib

English

If nth p n ≠ 0, then n < #hf.toFinset for hf : (setOf p).Finite.

Русский

Если nth p n ≠ 0, то n < #hf.toFinset при hf : (setOf p).Finite.

LaTeX

$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ {n}:\\\\mathbb{N},\\\\ nth\\\\ p\\\\ n \\\\neq 0 \\\\Rightarrow \\\\forall hf:\\\\{x:\\\\mathbb{N}\\\\mid p x\\\\}\\\\Finite,\\\\ n < #hf.toFinset.$$$

Lean4

theorem lt_card_toFinset_of_nth_ne_zero {n : ℕ} (h : nth p n ≠ 0) (hf : (setOf p).Finite) : n < #hf.toFinset :=
  by
  simp only [ne_eq, nth_eq_zero, not_or, not_exists, not_le] at h
  exact h.2 hf

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