mulSupport_eq_preimage

Mathlib.Algebra.Notation.Support

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

English

The set of x with f(x) ≠ 1 equals the complement of the preimage of {1} under f: mulSupport f = f^{-1}({1})^c.

Русский

Множество x с f(x) ≠ 1 равно комплементу предобраза {1} по f: mulSupport f = f^{-1}({1})^c.

LaTeX

$$$ \\mathrm{mulSupport}(f) = f^{-1}(\\{1\\})^{c} $$$

Lean4

@[to_additive]
theorem mulSupport_eq_preimage (f : ι → M) : mulSupport f = f ⁻¹' { 1 }ᶜ :=
  rfl

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

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

Разделы

Аффилиация

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