find_min

Mathlib.Data.Nat.Find

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

English

Every m with m < Nat.find(H) does not satisfy p.

Русский

Для каждого m < Nat.find(H) верно, что ¬p(m).

LaTeX

$$$\\forall m,\\ m < \\mathrm{Nat.find}(H) \\Rightarrow \\lnot p(m).$$$

Lean4

protected theorem find_min : ∀ {m : ℕ}, m < Nat.find H → ¬p m :=
  @(Nat.findX H).2.right

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

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

Разделы

Аффилиация

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