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_8) [topological_space M] [charted_space H M] (M' : Type u_9) [topological_space M'] [charted_space H' M'] (n : with_top ) :
Type (max u_8 u_9)

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

@[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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } :
has_coe_to_fun (M ≃ₘ^nI,I' M') (λ (_x : M ≃ₘ^nI,I' M'), M → M')
Equations
@[instance]
def diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } :
has_coe (M ≃ₘ^nI,I' M') C^nI, M; I', M'
Equations
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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (h : M ≃ₘ^nI,I' M') :
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (h : M ≃ₘ^nI,I' M') :
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (h : M ≃ₘ^nI,I' M') {x : M} :
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (h : M ≃ₘ^nI,I' M') {s : set M} {x : M} :
theorem diffeomorph.times_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 : E ≃ₘ^n𝓘(𝕜, E),𝓘(𝕜, E') E') :
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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] (h : M ≃ₘ^I,I' M') :
smooth I I' h
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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (h : M ≃ₘ^nI,I' M') (hn : 1 n) :
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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (h : M ≃ₘ^nI,I' M') (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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (h : M ≃ₘ^nI,I' M') :
@[simp]
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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (h : M ≃ₘ^nI,I' M') :
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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } {h h' : M ≃ₘ^nI,I' M'} :
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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } :
function.injective (λ (h : M ≃ₘ^nI,I' M') (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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } {h h' : M ≃ₘ^nI,I' M'} (Heq : ∀ (x : M), h x = h' x) :
h = h'
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_8) [topological_space M] [charted_space H M] (n : with_top ) :

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_8) [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_8) [topological_space M] [charted_space H M] (n : with_top ) :
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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h₁ : M ≃ₘ^nI,I' M') (h₂ : M' ≃ₘ^nI',J 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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (h : M ≃ₘ^nI,I' M') :
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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (h : M ≃ₘ^nI,I' M') :
@[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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h₁ : M ≃ₘ^nI,I' M') (h₂ : M' ≃ₘ^nI',J N) :
(h₁.trans h₂) = h₂ h₁
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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {n : with_top } :
@[simp]
theorem diffeomorph.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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J N) :
@[simp]
theorem diffeomorph.symm_trans {𝕜 : 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h₁ : M ≃ₘ^nI,I' M') (h₂ : M' ≃ₘ^nI',J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } {α : Sort u_3} (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J N) :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {N : Type u_10} [topological_space N] [charted_space G N] {n m : with_top } (h : M ≃ₘ^nI,J N) {f : N → M'} {s : set M} {x : M} (hm : m n) :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {N : Type u_10} [topological_space N] [charted_space G N] {n m : with_top } (h : M ≃ₘ^nI,J N) {f : N → M'} {s : set M} (hm : m n) :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {N : Type u_10} [topological_space N] [charted_space G N] {n m : with_top } (h : M ≃ₘ^nI,J N) {f : N → M'} {x : M} (hm : m n) :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {N : Type u_10} [topological_space N] [charted_space G N] {n m : with_top } (h : M ≃ₘ^nI,J N) {f : N → M'} (hm : m n) :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {N : Type u_10} [topological_space N] [charted_space G N] {n m : with_top } (h : M ≃ₘ^nI,J N) {f : M' → M} (hm : m n) {s : set M'} {x : M'} :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {N : Type u_10} [topological_space N] [charted_space G N] {n m : with_top } (h : M ≃ₘ^nI,J N) {f : M' → M} (hm : m n) {x : M'} :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {N : Type u_10} [topological_space N] [charted_space G N] {n m : with_top } (h : M ≃ₘ^nI,J N) {f : M' → M} (hm : m n) {s : set M'} :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {N : Type u_10} [topological_space N] [charted_space G N] {n m : with_top } (h : M ≃ₘ^nI,J N) {f : M' → M} (hm : m n) :
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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } (h : M ≃ₘ^nI,J N) (hn : 1 n) :
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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } [smooth_manifold_with_corners I M] [smooth_manifold_with_corners J N] (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } [smooth_manifold_with_corners I M] [smooth_manifold_with_corners J N] (h : M ≃ₘ^nI,J 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_8} [topological_space M] [charted_space H M] {N : Type u_10} [topological_space N] [charted_space G N] {n : with_top } [smooth_manifold_with_corners I M] [smooth_manifold_with_corners J N] (h : M ≃ₘ^nI,J 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 : E ≃ₘ^n𝓘(𝕜, E),𝓘(𝕜, F) F) (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 : E ≃ₘ^n𝓘(𝕜, E),𝓘(𝕜, F) F) (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 : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, E') E') :

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

Equations
@[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 : E ≃ₘ^𝓘(𝕜, 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 : E ≃ₘ^𝓘(𝕜, 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 : E ≃ₘ^𝓘(𝕜, 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_8} [topological_space M] [charted_space H M] (e : E ≃ₘ^𝓘(𝕜, 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_8} [topological_space M] [charted_space H M] (e : E ≃ₘ^𝓘(𝕜, 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_8} [topological_space M] [charted_space H M] (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, E') E') (x : M) :
@[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_8) [topological_space M] [charted_space H M] (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, F) F) :

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

Equations
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, F) F) {f : M' → M} {x : M'} {s : set M'} :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, F) F) {f : M' → M} {x : M'} :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, F) F) {f : M' → M} {s : set M'} :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, F) 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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, F) F) {f : M' → M} :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, F) F) {f : M → M'} {x : M} {s : set M} :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, F) F) {f : M → M'} {x : M} :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, F) F) {f : M → M'} {s : set M} :
@[simp]
theorem diffeomorph.times_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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] {n : with_top } (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, F) 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_8} [topological_space M] [charted_space H M] {M' : Type u_9} [topological_space M'] [charted_space H' M'] (e : E ≃ₘ^𝓘(𝕜, E),𝓘(𝕜, F) F) {f : M → M'} :