nth_false

Mathlib.Data.Nat.Nth

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

English

If p: ℕ → Prop is identically false, then nth p n = 0 for all n.

Русский

Пусть p: ℕ → Prop тождественно ложно; тогда для всех n выполняется nth p n = 0.

LaTeX

$$$$ \forall p:\mathbb{N}\to \mathsf{Prop}, \Big(\forall m, \neg p(m)\Big) \rightarrow \forall n, \operatorname{nth} p n = 0. $$$$

Lean4

@[simp]
theorem nth_false (n : ℕ) : nth (fun _ ↦ False) n = 0 :=
  nth_of_forall_not fun _ _ ↦ id

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

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

Разделы

Аффилиация

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