find_min'

Mathlib.Data.PNat.Find

URI: https://scilib.ai/kg/mathlib#PNat.find_min'

English

If p(m) holds, then find(h) ≤ m.

Русский

Если p(m) выполняется, то find(h) ≤ m.

LaTeX

$$$ \\forall m\\ (p(m) \\Rightarrow \\mathrm{PNat.find}(h) \\le m) $$$

Lean4

protected theorem find_min' {m : ℕ+} (hm : p m) : PNat.find h ≤ m :=
  le_of_not_gt fun l => PNat.find_min h l hm

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

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

Разделы

Аффилиация

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