lt_find

Mathlib.Data.Nat.PartENat

URI: https://scilib.ai/kg/mathlib#PartENat.lt_find

← MathLib Explorer

English

If, for all m ≤ n, not P m holds, then n < find P.

Русский

Если для всех m ≤ n верно ¬P(m), то n < find P.

LaTeX

$$$ (n : \mathbb{N}) \ (\forall m \le n, \neg P(m)) \Rightarrow (n : \mathrm{PartENat}) < \mathrm{find}(P) $$$

Lean4

theorem lt_find (n : ℕ) (h : ∀ m ≤ n, ¬P m) : (n : PartENat) < find P :=
  by
  rw [coe_lt_iff]
  intro h₁
  rw [find_get]
  have h₂ := @Nat.find_spec P _ h₁
  revert h₂
  contrapose!
  exact h _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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