mulSupport_div

Mathlib.Algebra.Group.Support

URI: https://scilib.ai/kg/mathlib#Function.mulSupport_div

← MathLib Explorer

English

The support of the quotient f x / g x is contained in the union of the supports of f and g.

Русский

Опора частного f/x / g/x содержится в объединении опор f и g.

LaTeX

$$mulSupport (fun x => f x / g x) ⊆ mulSupport f ∪ mulSupport g$$

Lean4

@[to_additive]
theorem mulSupport_div : (mulSupport fun x => f x / g x) ⊆ mulSupport f ∪ mulSupport g :=
  mulSupport_binop_subset (· / ·) one_div_one f g

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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