left_dom_of_mul_dom

Mathlib.Data.Part

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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