dom_of_le_of_dom

Mathlib.Data.Nat.PartENat

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

English

If x ≤ y and y is defined, then x is defined as well.

Русский

Если x ≤ y и y определён, то и x определён.

LaTeX

$$$\\\\forall {x y : PartENat}, x \\\\le y \\\\to y.\\\\Dom \\\\to x.\\\\Dom$$$

Lean4

theorem dom_of_le_of_dom {x y : PartENat} : x ≤ y → y.Dom → x.Dom := fun ⟨h, _⟩ => h

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

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

Разделы

Аффилиация

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