inv_toGerm — Mathlib

English

Let f be an almost everywhere invertible function taking values in a topological group γ. The inverse operation commutes with passing to germs, i.e., the germ of the inverse equals the inverse of the germ.

Русский

Пусть f является почти нигде инвертируемой функцией, принимающей значения в топологической группе γ. Операция взятия обратного и переход к Germ совместимы: Germ обращения равен обратному Germ.

LaTeX

$$$f^{-1}.toGerm = f.toGerm^{-1}$$$

Lean4

@[to_additive]
theorem inv_toGerm (f : α →ₘ[μ] γ) : f⁻¹.toGerm = f.toGerm⁻¹ :=
  comp_toGerm _ _ _

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