le_findGreatest

Mathlib.Data.Nat.Find

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

English

If m ≤ n then findGreatest P m ≤ findGreatest P n.

Русский

Если m ≤ n, то findGreatest P m ≤ findGreatest P n.

LaTeX

$$$m \le n \Rightarrow \mathrm{findGreatest} P m \le \mathrm{findGreatest} P n.$$$

Lean4

theorem le_findGreatest (hmb : m ≤ n) (hm : P m) : m ≤ Nat.findGreatest P n :=
  le_of_not_gt fun hlt => (findGreatest_eq_iff.1 rfl).2.2 hlt hmb hm

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

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

Разделы

Аффилиация

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