contMDiff_inclusion — Mathlib

English

The inclusion map from an open subset U of M into V ⊇ U is C^n.

Русский

Включение из открытого подмножества U в V ⊇ U является C^n.

LaTeX

$$ContMDiff I I n (Opens.inclusion h)$$

Lean4

theorem contMDiff_inclusion {n : WithTop ℕ∞} {U V : Opens M} (h : U ≤ V) :
    ContMDiff I I n (Opens.inclusion h : U → V) :=
  by
  rintro ⟨x, hx : x ∈ U⟩
  apply (contDiffWithinAt_localInvariantProp n).liftProp_inclusion
  intro y
  dsimp only [ContDiffWithinAtProp, id_comp, preimage_univ]
  rw [Set.univ_inter]
  exact contDiffWithinAt_id.congr I.rightInvOn (congr_arg I (I.left_inv y))

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