instContMDiffInv₀OfNatWithTopENatOfContinuousInv₀

English

Dual statement about ContMDiffInv₀ for Nat with ENat top.

Русский

Двойственное утверждение для ContMDiffInv₀ на Nat с ENат top.

LaTeX

$$ContMDiffInv₀ I 0 G$$

Lean4

instance [ContinuousInv₀ G] : ContMDiffInv₀ I 0 G :=
  by
  have : T1Space G := I.t1Space G
  constructor
  have A : ContMDiffOn I I 0 (fun (x : G) ↦ x⁻¹) {0}ᶜ :=
    by
    rw [contMDiffOn_zero_iff]
    exact continuousOn_inv₀
  intro x hx
  have : ContMDiffWithinAt I I 0 (fun (x : G) ↦ x⁻¹) {0}ᶜ x := A x hx
  apply ContMDiffWithinAt.contMDiffAt this
  exact IsOpen.mem_nhds isOpen_compl_singleton hx

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