support_inv' — Mathlib

English

Let I be an index set and G a group with zero. For any f: I → G, the support of the inverse-valued function equals the support of f.

Русский

Пусть I — множество индексов и G — группа с нулём. Для любой функции f: I → G опора функции a ↦ f(a)^{-1} равна опоре f.

LaTeX

$$$\\operatorname{supp}(f^{-1}) = \\operatorname{supp}(f)$$$

Lean4

@[simp]
theorem support_inv' (f : ι → G₀) : support f⁻¹ = support f :=
  support_inv _

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