find_eq_top_iff

Mathlib.Data.Nat.PartENat

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

← MathLib Explorer

English

The predicate find P equals the top element iff P is false for all n.

Русский

predicat find P равен вершине тогда и только тогда, когда P(n) ложно для всех n.

LaTeX

$$$ find P = \top \iff \forall n, \neg P n $$$

Lean4

theorem find_eq_top_iff : find P = ⊤ ↔ ∀ n, ¬P n :=
  (eq_top_iff_forall_lt _).trans ⟨fun h n => (lt_find_iff P n).mp (h n) _ le_rfl, fun h n => lt_find P n fun _ _ => h _⟩

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

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

Разделы

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

Аффилиация

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