one_le_find

Mathlib.Data.PNat.Find

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

English

The lemma shows that find h is greater than 1 iff p(1) is false.

Русский

Лемма показывает, что find h больше 1 тогда когда p(1) ложно.

LaTeX

$$$ 1 < \\mathrm{PNat.find}(h) \\iff \\neg p(1) $$$

Lean4

theorem one_le_find : 1 < PNat.find h ↔ ¬p 1 := by simp

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

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

Разделы

Аффилиация

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