mulSupport_comp_eq_preimage

Mathlib.Algebra.Notation.Support

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

English

The mulSupport of the composition equals the preimage of the mulSupport of g under f.

Русский

Опора композиции равна предобразу опоры g под f.

LaTeX

$$$ \operatorname{mulSupport}(g \circ f) = f^{-1}(\operatorname{mulSupport}(g)) $$$

Lean4

@[to_additive]
theorem mulSupport_comp_eq_preimage (g : κ → M) (f : ι → κ) : mulSupport (g ∘ f) = f ⁻¹' mulSupport g :=
  rfl

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

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

Разделы

Аффилиация

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