dom_of_le_natCast

Mathlib.Data.Nat.PartENat

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

English

If x is bounded above by y cast to PartENat, then x has a representation in the domain.

Русский

Если x ограничено сверху конвертацией y из ℕ в PartENat, то x принадлежит области определения.

LaTeX

$$$ x \le \hat{y} \Rightarrow \mathrm{Dom}(x) $$$

Lean4

theorem dom_of_le_natCast {x : PartENat} {y : ℕ} (h : x ≤ y) : x.Dom := by exact dom_of_le_some h

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

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

Разделы

Аффилиация

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