nth_mem_of_ne_zero

Mathlib.Data.Nat.Nth

URI: https://scilib.ai/kg/mathlib#Nat.nth_mem_of_ne_zero

← MathLib Explorer

English

If nth p n ≠ 0, then p(nth p n) holds.

Русский

Если nth p n ≠ 0, то выполняется p(nth p n).

LaTeX

$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ {n}:\\\\mathbb{N},\\\\ nth\\\\ p\\\\ n \\\\neq 0 \\\\Rightarrow \\\\ p\\\\ (\\\\mathrm{nth}\\\\ p\\\\ n).$$$

Lean4

theorem nth_mem_of_ne_zero {n : ℕ} (h : nth p n ≠ 0) : p (Nat.nth p n) :=
  nth_mem n (lt_card_toFinset_of_nth_ne_zero h)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru