find_spec

Mathlib.Data.Nat.Find

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

English

Nat.find yields a witness for p; i.e., p(Nat.find(H)).

Русский

Nat.find дает свидетельство для p; то есть p(Nat.find(H)).

LaTeX

$$$p(\\mathrm{Nat.find}(H)).$$$

Lean4

protected theorem find_spec : p (Nat.find H) :=
  (Nat.findX H).2.left

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

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

Разделы

Аффилиация

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