support_inv — Mathlib

English

Let I be an index set and G a group with zero. For every function f: I → G, the support of the inverse-valued function a ↦ f(a)^{-1} equals the support of f.

Русский

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

LaTeX

$$$\\operatorname{supp}\\bigl(a \\mapsto f(a)^{-1}\\bigr) = \\operatorname{supp}(f)$$$

Lean4

@[simp]
theorem support_inv (f : ι → G₀) : support (fun a ↦ (f a)⁻¹) = support f :=
  Set.ext fun _ ↦ not_congr inv_eq_zero

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