tsupport_mul_subset_right

Mathlib.Topology.Algebra.Support

URI: https://scilib.ai/kg/mathlib#tsupport_mul_subset_right

← MathLib Explorer

English

The tsupport of the product f x g is contained in the tsupport of g: tsupport (f·g) ⊆ tsupport g.

Русский

Опора-погл. произведения ⟶ tsupport g.

LaTeX

$$$\operatorname{tsupport}(x \mapsto f(x) \cdot g(x)) \subseteq \operatorname{tsupport}(g)$$$

Lean4

theorem tsupport_mul_subset_right {α : Type*} [MulZeroClass α] {f g : X → α} :
    (tsupport fun x => f x * g x) ⊆ tsupport g :=
  closure_mono (support_mul_subset_right _ _)

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

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

Разделы

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

Аффилиация

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