right_dom_of_mul_dom

Mathlib.Data.Part

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

English

If the product a * b has a domain, then b.Dom holds.

Русский

Если произведение a * b имеет домен, то b обладает областью определения.

LaTeX

$$$ (a * b).Dom \rightarrow b.Dom $$$

Lean4

@[to_additive]
theorem right_dom_of_mul_dom [Mul α] {a b : Part α} (hab : Dom (a * b)) : b.Dom :=
  hab.2

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

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

Разделы

Аффилиация

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