find

Mathlib.Data.Nat.PartENat

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

English

The smallest PartENat satisfying a decidable predicate P on ℕ is defined as find P.

Русский

Наименьшее Element PartENat, удовлетворяющее DecidablePred P на Naturals, задаётся как find P.

LaTeX

$$$ find : (\mathbb{N} \to \text{Prop}) \to \mathrm{PartENat} $$$

Lean4

/-- The smallest `PartENat` satisfying a (decidable) predicate `P : ℕ → Prop` -/
def find : PartENat :=
  ⟨∃ n, P n, Nat.find⟩

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

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

Разделы

Аффилиация

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