le_find_iff

Mathlib.Data.Nat.Find

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

← MathLib Explorer

English

n ≤ Nat.find(h) is equivalent to ∀ m < n, ¬p(m).

Русский

n ≤ Nat.find(h) эквивалентно ∀ m < n, ¬p(m).

LaTeX

$$$n \\le \\mathrm{Nat.find}(h) \\iff \\forall m < n, \\lnot p(m).$$$

Lean4

@[simp]
theorem le_find_iff (h : ∃ n : ℕ, p n) (n : ℕ) : n ≤ Nat.find h ↔ ∀ m < n, ¬p m := by
  simp only [← not_lt, find_lt_iff, not_exists, not_and]

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

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

Разделы

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

Аффилиация

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