lt_find_iff

Mathlib.Data.Nat.Find

URI: https://scilib.ai/kg/mathlib#Nat.lt_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 < \\mathrm{Nat.find}(h) \\iff \\forall m \\le n, \\lnot p(m).$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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