nth_zero

Mathlib.Data.Nat.Nth

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

English

For any p, nth p 0 equals the least element of setOf p, i.e., sInf(setOf p).

Русский

Для произвольного p, nth p 0 равен наименьшему элементу множества {n | p n}.

LaTeX

$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}},\\\\ nth\\\\ p\\\\ 0 =\\\\ sInf\\\\(\\\\{x \\\\mid p x\\\\}).$$$

Lean4

theorem nth_zero : nth p 0 = sInf (setOf p) := by rw [nth_eq_sInf]; simp

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

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

Разделы

Аффилиация

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