find_dom

Mathlib.Data.Nat.PartENat

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

English

For predicate P, if there exists n with P n, then (find P).Dom holds.

Русский

Для предиката P, если существует n, такое что P n, то (find P).Dom выполняется.

LaTeX

$$$ (\exists n, P(n)) \Rightarrow (\text{find } P).Dom $$$

Lean4

theorem find_dom (h : ∃ n, P n) : (find P).Dom :=
  h

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

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

Разделы

Аффилиация

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