mathlib documentation

geometry.manifold.diffeomorph

Diffeomorphisms #

This file implements diffeomorphisms.

Definitions #

Notations #

Implementation notes #

This notion of diffeomorphism is needed although there is already a notion of structomorphism because structomorphisms do not allow the model spaces H and H' of the two manifolds to be different, i.e. for a structomorphism one has to impose H = H' which is often not the case in practice.

Keywords #

diffeomorphism, manifold

@[nolint]
structure diffeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] (I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H') (M : Type u_9) [topological_space M] [charted_space H M] (M' : Type u_10) [topological_space M'] [charted_space H' M'] (n : with_top ) :
Type (max u_10 u_9)

n-times continuously differentiable diffeomorphism between M and M' with respect to I and I'

Instances for diffeomorph
@[protected, instance]
def diffeomorph.has_coe_to_fun {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } :
has_coe_to_fun (diffeomorph I I' M M' n) (λ (_x : diffeomorph I I' M M' n), M → M')
Equations
@[protected, instance]
def diffeomorph.cont_mdiff_map.has_coe {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } :
has_coe (diffeomorph I I' M M' n) (cont_mdiff_map I I' M M' n)
Equations
@[protected, continuity]
theorem diffeomorph.continuous {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (h : diffeomorph I I' M M' n) :
@[protected]
theorem diffeomorph.cont_mdiff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (h : diffeomorph I I' M M' n) :
cont_mdiff I I' n h
@[protected]
theorem diffeomorph.cont_mdiff_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (h : diffeomorph I I' M M' n) {x : M} :
cont_mdiff_at I I' n h x
@[protected]
theorem diffeomorph.cont_mdiff_within_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (h : diffeomorph I I' M M' n) {s : set M} {x : M} :
@[protected]
theorem diffeomorph.cont_diff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {n : with_top } (h : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' n) :
cont_diff 𝕜 n h
@[protected]
theorem diffeomorph.smooth {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] (h : diffeomorph I I' M M' ) :
smooth I I' h
@[protected]
theorem diffeomorph.mdifferentiable {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (h : diffeomorph I I' M M' n) (hn : 1 n) :
@[protected]
theorem diffeomorph.mdifferentiable_on {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (h : diffeomorph I I' M M' n) (s : set M) (hn : 1 n) :
@[simp]
theorem diffeomorph.coe_to_equiv {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (h : diffeomorph I I' M M' n) :
@[simp, norm_cast]
theorem diffeomorph.coe_coe {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (h : diffeomorph I I' M M' n) :
theorem diffeomorph.to_equiv_injective {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } :
@[simp]
theorem diffeomorph.to_equiv_inj {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } {h h' : diffeomorph I I' M M' n} :
h.to_equiv = h'.to_equiv h = h'
theorem diffeomorph.coe_fn_injective {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } :
function.injective (λ (h : diffeomorph I I' M M' n) (x : M), h x)

Coercion to function λ h : M ≃ₘ^n⟮I, I'⟯ M', (h : M → M') is injective.

@[ext]
theorem diffeomorph.ext {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } {h h' : diffeomorph I I' M M' n} (Heq : ∀ (x : M), h x = h' x) :
h = h'
@[protected]
def diffeomorph.refl {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_5} [topological_space H] (I : model_with_corners 𝕜 E H) (M : Type u_9) [topological_space M] [charted_space H M] (n : with_top ) :
diffeomorph I I M M n

Identity map as a diffeomorphism.

Equations
@[simp]
theorem diffeomorph.refl_to_equiv {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_5} [topological_space H] (I : model_with_corners 𝕜 E H) (M : Type u_9) [topological_space M] [charted_space H M] (n : with_top ) :
@[simp]
theorem diffeomorph.coe_refl {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_5} [topological_space H] (I : model_with_corners 𝕜 E H) (M : Type u_9) [topological_space M] [charted_space H M] (n : with_top ) :
@[protected]
def diffeomorph.trans {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h₁ : diffeomorph I I' M M' n) (h₂ : diffeomorph I' J M' N n) :
diffeomorph I J M N n

Composition of two diffeomorphisms.

Equations
@[simp]
theorem diffeomorph.trans_refl {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (h : diffeomorph I I' M M' n) :
h.trans (diffeomorph.refl I' M' n) = h
@[simp]
theorem diffeomorph.refl_trans {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (h : diffeomorph I I' M M' n) :
@[simp]
theorem diffeomorph.coe_trans {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h₁ : diffeomorph I I' M M' n) (h₂ : diffeomorph I' J M' N n) :
(h₁.trans h₂) = h₂ h₁
@[protected]
def diffeomorph.symm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) :
diffeomorph J I N M n

Inverse of a diffeomorphism.

Equations
@[simp]
theorem diffeomorph.apply_symm_apply {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) (x : N) :
h ((h.symm) x) = x
@[simp]
theorem diffeomorph.symm_apply_apply {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) (x : M) :
(h.symm) (h x) = x
@[simp]
theorem diffeomorph.symm_refl {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_5} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_9} [topological_space M] [charted_space H M] {n : with_top } :
@[simp]
theorem diffeomorph.self_trans_symm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) :
@[simp]
theorem diffeomorph.symm_trans_self {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) :
@[simp]
theorem diffeomorph.symm_trans' {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h₁ : diffeomorph I I' M M' n) (h₂ : diffeomorph I' J M' N n) :
(h₁.trans h₂).symm = h₂.symm.trans h₁.symm
@[simp]
theorem diffeomorph.symm_to_equiv {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) :
@[simp]
theorem diffeomorph.to_equiv_coe_symm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) :
theorem diffeomorph.image_eq_preimage {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) (s : set M) :
h '' s = (h.symm) ⁻¹' s
theorem diffeomorph.symm_image_eq_preimage {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) (s : set N) :
(h.symm) '' s = h ⁻¹' s
@[simp]
theorem diffeomorph.range_comp {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } {α : Sort u_3} (h : diffeomorph I J M N n) (f : α → M) :
@[simp]
theorem diffeomorph.image_symm_image {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) (s : set N) :
h '' ((h.symm) '' s) = s
@[simp]
theorem diffeomorph.symm_image_image {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) (s : set M) :
(h.symm) '' (h '' s) = s
def diffeomorph.to_homeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) :
M ≃ₜ N

A diffeomorphism is a homeomorphism.

Equations
@[simp]
theorem diffeomorph.to_homeomorph_to_equiv {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) :
@[simp]
theorem diffeomorph.symm_to_homeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) :
@[simp]
theorem diffeomorph.coe_to_homeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) :
@[simp]
theorem diffeomorph.coe_to_homeomorph_symm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) :
@[simp]
theorem diffeomorph.cont_mdiff_within_at_comp_diffeomorph_iff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {n m : with_top } (h : diffeomorph I J M N n) {f : N → M'} {s : set M} {x : M} (hm : m n) :
cont_mdiff_within_at I I' m (f h) s x cont_mdiff_within_at J I' m f ((h.symm) ⁻¹' s) (h x)
@[simp]
theorem diffeomorph.cont_mdiff_on_comp_diffeomorph_iff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {n m : with_top } (h : diffeomorph I J M N n) {f : N → M'} {s : set M} (hm : m n) :
cont_mdiff_on I I' m (f h) s cont_mdiff_on J I' m f ((h.symm) ⁻¹' s)
@[simp]
theorem diffeomorph.cont_mdiff_at_comp_diffeomorph_iff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {n m : with_top } (h : diffeomorph I J M N n) {f : N → M'} {x : M} (hm : m n) :
cont_mdiff_at I I' m (f h) x cont_mdiff_at J I' m f (h x)
@[simp]
theorem diffeomorph.cont_mdiff_comp_diffeomorph_iff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {n m : with_top } (h : diffeomorph I J M N n) {f : N → M'} (hm : m n) :
cont_mdiff I I' m (f h) cont_mdiff J I' m f
@[simp]
theorem diffeomorph.cont_mdiff_within_at_diffeomorph_comp_iff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {n m : with_top } (h : diffeomorph I J M N n) {f : M' → M} (hm : m n) {s : set M'} {x : M'} :
cont_mdiff_within_at I' J m (h f) s x cont_mdiff_within_at I' I m f s x
@[simp]
theorem diffeomorph.cont_mdiff_at_diffeomorph_comp_iff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {n m : with_top } (h : diffeomorph I J M N n) {f : M' → M} (hm : m n) {x : M'} :
cont_mdiff_at I' J m (h f) x cont_mdiff_at I' I m f x
@[simp]
theorem diffeomorph.cont_mdiff_on_diffeomorph_comp_iff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {n m : with_top } (h : diffeomorph I J M N n) {f : M' → M} (hm : m n) {s : set M'} :
cont_mdiff_on I' J m (h f) s cont_mdiff_on I' I m f s
@[simp]
theorem diffeomorph.cont_mdiff_diffeomorph_comp_iff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {n m : with_top } (h : diffeomorph I J M N n) {f : M' → M} (hm : m n) :
cont_mdiff I' J m (h f) cont_mdiff I' I m f
theorem diffeomorph.to_local_homeomorph_mdifferentiable {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } (h : diffeomorph I J M N n) (hn : 1 n) :
def diffeomorph.prod_congr {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {G' : Type u_8} [topological_space G'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {J' : model_with_corners 𝕜 F G'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {N' : Type u_12} [topological_space N'] [charted_space G' N'] {n : with_top } (h₁ : diffeomorph I I' M M' n) (h₂ : diffeomorph J J' N N' n) :
diffeomorph (I.prod J) (I'.prod J') (M × N) (M' × N') n

Product of two diffeomorphisms.

Equations
@[simp]
theorem diffeomorph.prod_congr_symm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {G' : Type u_8} [topological_space G'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {J' : model_with_corners 𝕜 F G'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {N' : Type u_12} [topological_space N'] [charted_space G' N'] {n : with_top } (h₁ : diffeomorph I I' M M' n) (h₂ : diffeomorph J J' N N' n) :
(h₁.prod_congr h₂).symm = h₁.symm.prod_congr h₂.symm
@[simp]
theorem diffeomorph.coe_prod_congr {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] {G' : Type u_8} [topological_space G'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {J : model_with_corners 𝕜 F G} {J' : model_with_corners 𝕜 F G'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {N : Type u_11} [topological_space N] [charted_space G N] {N' : Type u_12} [topological_space N'] [charted_space G' N'] {n : with_top } (h₁ : diffeomorph I I' M M' n) (h₂ : diffeomorph J J' N N' n) :
(h₁.prod_congr h₂) = prod.map h₁ h₂
def diffeomorph.prod_comm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] (I : model_with_corners 𝕜 E H) (J : model_with_corners 𝕜 F G) (M : Type u_9) [topological_space M] [charted_space H M] (N : Type u_11) [topological_space N] [charted_space G N] (n : with_top ) :
diffeomorph (I.prod J) (J.prod I) (M × N) (N × M) n

M × N is diffeomorphic to N × M.

Equations
@[simp]
theorem diffeomorph.prod_comm_symm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] (I : model_with_corners 𝕜 E H) (J : model_with_corners 𝕜 F G) (M : Type u_9) [topological_space M] [charted_space H M] (N : Type u_11) [topological_space N] [charted_space G N] (n : with_top ) :
@[simp]
theorem diffeomorph.coe_prod_comm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] (I : model_with_corners 𝕜 E H) (J : model_with_corners 𝕜 F G) (M : Type u_9) [topological_space M] [charted_space H M] (N : Type u_11) [topological_space N] [charted_space G N] (n : with_top ) :
def diffeomorph.prod_assoc {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {G' : Type u_8} [topological_space G'] (I : model_with_corners 𝕜 E H) (J : model_with_corners 𝕜 F G) (J' : model_with_corners 𝕜 F G') (M : Type u_9) [topological_space M] [charted_space H M] (N : Type u_11) [topological_space N] [charted_space G N] (N' : Type u_12) [topological_space N'] [charted_space G' N'] (n : with_top ) :
diffeomorph ((I.prod J).prod J') (I.prod (J.prod J')) ((M × N) × N') (M × N × N') n

(M × N) × N' is diffeomorphic to M × (N × N').

Equations
theorem diffeomorph.unique_mdiff_on_image_aux {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } [smooth_manifold_with_corners I M] [smooth_manifold_with_corners J N] (h : diffeomorph I J M N n) (hn : 1 n) {s : set M} (hs : unique_mdiff_on I s) :
@[simp]
theorem diffeomorph.unique_mdiff_on_image {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } [smooth_manifold_with_corners I M] [smooth_manifold_with_corners J N] (h : diffeomorph I J M N n) (hn : 1 n) {s : set M} :
@[simp]
theorem diffeomorph.unique_mdiff_on_preimage {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] {I : model_with_corners 𝕜 E H} {J : model_with_corners 𝕜 F G} {M : Type u_9} [topological_space M] [charted_space H M] {N : Type u_11} [topological_space N] [charted_space G N] {n : with_top } [smooth_manifold_with_corners I M] [smooth_manifold_with_corners J N] (h : diffeomorph I J M N n) (hn : 1 n) {s : set N} :
@[simp]
theorem diffeomorph.unique_diff_on_image {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {n : with_top } (h : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F n) (hn : 1 n) {s : set E} :
@[simp]
theorem diffeomorph.unique_diff_on_preimage {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {n : with_top } (h : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F n) (hn : 1 n) {s : set F} :
def continuous_linear_equiv.to_diffeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] (e : E ≃L[𝕜] E') :

A continuous linear equivalence between normed spaces is a diffeomorphism.

Equations
@[simp]
theorem continuous_linear_equiv.coe_to_diffeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] (e : E ≃L[𝕜] E') :
@[simp]
theorem continuous_linear_equiv.symm_to_diffeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] (e : E ≃L[𝕜] E') :
@[simp]
theorem continuous_linear_equiv.coe_to_diffeomorph_symm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] (e : E ≃L[𝕜] E') :
def model_with_corners.trans_diffeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] (I : model_with_corners 𝕜 E H) (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' ) :

Apply a diffeomorphism (e.g., a continuous linear equivalence) to the model vector space.

Equations
Instances for model_with_corners.trans_diffeomorph
@[simp]
theorem model_with_corners.coe_trans_diffeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] (I : model_with_corners 𝕜 E H) (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' ) :
@[simp]
theorem model_with_corners.coe_trans_diffeomorph_symm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] (I : model_with_corners 𝕜 E H) (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' ) :
theorem model_with_corners.trans_diffeomorph_range {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] (I : model_with_corners 𝕜 E H) (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' ) :
theorem model_with_corners.coe_ext_chart_at_trans_diffeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_9} [topological_space M] [charted_space H M] (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' ) (x : M) :
theorem model_with_corners.coe_ext_chart_at_trans_diffeomorph_symm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_9} [topological_space M] [charted_space H M] (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' ) (x : M) :
theorem model_with_corners.ext_chart_at_trans_diffeomorph_target {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_9} [topological_space M] [charted_space H M] (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' ) (x : M) :
@[protected, instance]
def diffeomorph.to_trans_diffeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] (I : model_with_corners 𝕜 E H) (M : Type u_9) [topological_space M] [charted_space H M] (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ) :

The identity diffeomorphism between a manifold with model I and the same manifold with model I.trans_diffeomorph e.

Equations
@[simp]
theorem diffeomorph.cont_mdiff_within_at_trans_diffeomorph_right {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ) {f : M' → M} {x : M'} {s : set M'} :
@[simp]
theorem diffeomorph.cont_mdiff_at_trans_diffeomorph_right {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ) {f : M' → M} {x : M'} :
@[simp]
theorem diffeomorph.cont_mdiff_on_trans_diffeomorph_right {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ) {f : M' → M} {s : set M'} :
@[simp]
theorem diffeomorph.cont_mdiff_trans_diffeomorph_right {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ) {f : M' → M} :
@[simp]
theorem diffeomorph.smooth_trans_diffeomorph_right {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ) {f : M' → M} :
@[simp]
theorem diffeomorph.cont_mdiff_within_at_trans_diffeomorph_left {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ) {f : M → M'} {x : M} {s : set M} :
@[simp]
theorem diffeomorph.cont_mdiff_at_trans_diffeomorph_left {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ) {f : M → M'} {x : M} :
@[simp]
theorem diffeomorph.cont_mdiff_on_trans_diffeomorph_left {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ) {f : M → M'} {s : set M} :
@[simp]
theorem diffeomorph.cont_mdiff_trans_diffeomorph_left {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] {n : with_top } (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ) {f : M → M'} :
@[simp]
theorem diffeomorph.smooth_trans_diffeomorph_left {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_9} [topological_space M] [charted_space H M] {M' : Type u_10} [topological_space M'] [charted_space H' M'] (e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ) {f : M → M'} :