find_min'

Mathlib.Data.Nat.Find

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

English

If p(m) holds, then Nat.find(H) ≤ m.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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