dom_some

Mathlib.Data.Nat.PartENat

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

English

For every n ∈ ℕ, the element some n is defined in PartENat; i.e., it lies in the domain.

Русский

Для каждого натурального числа n элемент some n определён в PartENat; принадлежит области определения.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}, (\\\\mathrm{some}\\\\, n).\\\\Dom$$$

Lean4

@[simp]
theorem dom_some (x : ℕ) : (some x).Dom :=
  trivial

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

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

Разделы

Аффилиация

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