dom_of_lt

Mathlib.Data.Nat.PartENat

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

English

If x < y, then x has a domain (x.Dom).

Русский

Если x < y, то x имеет область определения (x.Dom).

LaTeX

$$$ x < y \Rightarrow x.Dom $$$

Lean4

theorem dom_of_lt {x y : PartENat} : x < y → x.Dom :=
  PartENat.casesOn x not_top_lt fun _ _ => dom_natCast _

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

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

Разделы

Аффилиация

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