right_dom_of_append_dom

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.right_dom_of_append_dom

English

If a ++ b is defined, then b has a domain.

Русский

Если a ++ b определено, тогда b имеет домен.

LaTeX

$$$$ \operatorname{Dom}(a \!\!\+\!\!\! b) \Rightarrow \operatorname{Dom}(b). $$$$

Lean4

theorem right_dom_of_append_dom [Append α] {a b : Part α} (hab : Dom (a ++ b)) : b.Dom :=
  hab.2

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

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

Разделы

Аффилиация

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