support_mul_subset_right

Mathlib.Algebra.GroupWithZero.Indicator

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

English

For any f,g: ι → M₀, the support of the product f · g is contained in the support of g.

Русский

Для любых f,g: ι → M₀ опора произведения ⟨f,g⟩ ⊆ опора g.

LaTeX

$$$ \operatorname{support}(f \cdot g) \subseteq \operatorname{support}(g). $$$

Lean4

theorem support_mul_subset_right (f g : ι → M₀) : support (fun x ↦ f x * g x) ⊆ support g := fun x hfg hg =>
  hfg <| by simp only [hg, mul_zero]

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

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

Разделы

Аффилиация

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