find_spec

Mathlib.Data.PNat.Find

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

English

The chosen witness N = PNat.find h satisfies p(N).

Русский

Выбранный свидетель N = PNat.find h удовлетворяет p(N).

LaTeX

$$$ p( \\mathrm{PNat.find}(h) ) $$$

Lean4

protected theorem find_spec : p (PNat.find h) :=
  (PNat.findX h).prop.left

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

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

Разделы

Аффилиация

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