English
Let f be a smooth map on a set s, taking values in a group where inverse is defined. If f is C^n on s and f(x) ≠ e (the identity) for all x in s, then the map x ↦ f(x)^{-1} is also C^n on s.
Русский
Пусть f — гладкое отображение на области s с значениями в группы, у которой существует обратное. Если f гладко по классу C^n на s и для всех x∈s f(x) не равна единице, то отображение x ↦ f(x)^{-1} также гладко по классу C^n на s.
LaTeX
$$$$ \ContMDiffOn I' I n f s \quad\land\quad (\forall x\in s\, f(x) \neq 0) \Rightarrow \ContMDiffOn I' I n \bigl( \lambda x \mapsto (f(x))^{-1} \bigr) s $$$$
Lean4
theorem inv₀ (hf : ContMDiffOn I' I n f s) (h0 : ∀ x ∈ s, f x ≠ 0) : ContMDiffOn I' I n (fun x => (f x)⁻¹) s :=
fun x hx ↦ ContMDiffWithinAt.inv₀ (hf x hx) (h0 x hx)
