instContMDiffInv₀ModelWithCornersSelf

English

If a ContMDiffInv₀ structure exists at level n, then it also exists at every lower level m ≤ n.

Русский

Если существует структура ContMDiffInv₀ на уровне n, то она существует и на любом нижнем уровне m ≤ n.

LaTeX

$$ContMDiffInv₀ I n G → m ≤ n → ContMDiffInv₀ I m G$$

Lean4

instance {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : ContMDiffInv₀ 𝓘(𝕜) n 𝕜 where
  contMDiffAt_inv₀ x
    hx := by
    change ContMDiffAt 𝓘(𝕜) 𝓘(𝕜) n Inv.inv x
    rw [contMDiffAt_iff_contDiffAt]
    exact contDiffAt_inv 𝕜 hx

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