Diffeomorphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file implements diffeomorphisms.
Definitions #
diffeomorph I I' M M' n:n-times continuously differentiable diffeomorphism betweenMandM'with respect to I and I'; we do not introduce a separate definition for the casen = ∞; we use notation instead.diffeomorph.to_homeomorph: reinterpret a diffeomorphism as a homeomorphism.continuous_linear_equiv.to_diffeomorph: reinterpret a continuous equivalence as a diffeomorphism.model_with_corners.trans_diffeomorph: compose a givenmodel_with_cornerswith a diffeomorphism between the old and the new target spaces. Useful, e.g, to turn any finite dimensional manifold into a manifold modelled on a Euclidean space.diffeomorph.to_trans_diffeomorph: the identity diffeomorphism betweenMwith modelIandMwith modelI.trans_diffeomorph e.
Notations #
M ≃ₘ^n⟮I, I'⟯ M':=diffeomorph I J M N nM ≃ₘ⟮I, I'⟯ M':=diffeomorph I J M N ⊤E ≃ₘ^n[𝕜] E':=E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'E ≃ₘ[𝕜] E':=E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞) :
Type (max u_10 u_9)
- to_equiv : M ≃ M'
- cont_mdiff_to_fun : cont_mdiff I I' n ⇑(self.to_equiv)
- cont_mdiff_inv_fun : cont_mdiff I' I n ⇑(self.to_equiv.symm)
n-times continuously differentiable diffeomorphism between M and M' with respect to I and I'
Instances for diffeomorph
- diffeomorph.has_sizeof_inst
- diffeomorph.has_coe_to_fun
- diffeomorph.cont_mdiff_map.has_coe
- diffeomorph.continuous_map_class
@[protected, instance]
def
diffeomorph.has_coe_to_fun
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞} :
has_coe_to_fun (diffeomorph I I' M M' n) (λ (_x : diffeomorph I I' M M' n), M → M')
Equations
- diffeomorph.has_coe_to_fun = {coe := λ (e : diffeomorph I I' M M' n), ⇑(e.to_equiv)}
@[protected, instance]
def
diffeomorph.cont_mdiff_map.has_coe
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞} :
has_coe (diffeomorph I I' M M' n) (cont_mdiff_map I I' M M' n)
Equations
- diffeomorph.cont_mdiff_map.has_coe = {coe := λ (Φ : diffeomorph I I' M M' n), ⟨⇑Φ, _⟩}
@[protected, continuity]
theorem
diffeomorph.continuous
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I I' M M' n) :
@[protected]
theorem
diffeomorph.cont_mdiff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I I' M M' n) :
cont_mdiff I I' n ⇑h
@[protected]
theorem
diffeomorph.cont_mdiff_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
(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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I I' M M' n)
{s : set M}
{x : M} :
cont_mdiff_within_at I I' n ⇑h s x
@[protected]
theorem
diffeomorph.cont_diff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
(h : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' n) :
@[protected]
theorem
diffeomorph.smooth
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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' ⊤) :
@[protected]
theorem
diffeomorph.mdifferentiable
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I I' M M' n)
(hn : 1 ≤ n) :
mdifferentiable I I' ⇑h
@[protected]
theorem
diffeomorph.mdifferentiable_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I I' M M' n)
(s : set M)
(hn : 1 ≤ n) :
mdifferentiable_on I I' ⇑h s
@[simp]
theorem
diffeomorph.coe_to_equiv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I I' M M' n) :
@[simp, norm_cast]
theorem
diffeomorph.coe_coe
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I I' M M' n) :
theorem
diffeomorph.to_equiv_injective
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞} :
@[simp]
theorem
diffeomorph.to_equiv_inj
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
{h h' : diffeomorph I I' M M' n} :
theorem
diffeomorph.coe_fn_injective
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞} :
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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
{h h' : diffeomorph I I' M M' n}
(Heq : ∀ (x : M), ⇑h x = ⇑h' x) :
h = h'
@[protected, instance]
def
diffeomorph.continuous_map_class
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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] :
continuous_map_class (diffeomorph I J M N ⊤) M N
Equations
@[protected]
def
diffeomorph.refl
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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 : ℕ∞) :
diffeomorph I I M M n
Identity map as a diffeomorphism.
Equations
- diffeomorph.refl I M n = {to_equiv := equiv.refl M, cont_mdiff_to_fun := _, cont_mdiff_inv_fun := _}
@[simp]
theorem
diffeomorph.refl_to_equiv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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 : ℕ∞) :
(diffeomorph.refl I M n).to_equiv = equiv.refl M
@[simp]
theorem
diffeomorph.coe_refl
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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 : ℕ∞) :
⇑(diffeomorph.refl I M n) = id
@[protected]
def
diffeomorph.trans
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(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
- h₁.trans h₂ = {to_equiv := h₁.to_equiv.trans h₂.to_equiv, cont_mdiff_to_fun := _, cont_mdiff_inv_fun := _}
@[simp]
theorem
diffeomorph.trans_refl
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I I' M M' n) :
h.trans (diffeomorph.refl I' M' n) = h
@[simp]
theorem
diffeomorph.refl_trans
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I I' M M' n) :
(diffeomorph.refl I M n).trans h = h
@[simp]
theorem
diffeomorph.coe_trans
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h₁ : diffeomorph I I' M M' n)
(h₂ : diffeomorph I' J M' N n) :
@[protected]
def
diffeomorph.symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n) :
diffeomorph J I N M n
Inverse of a diffeomorphism.
Equations
- h.symm = {to_equiv := h.to_equiv.symm, cont_mdiff_to_fun := _, cont_mdiff_inv_fun := _}
@[simp]
theorem
diffeomorph.apply_symm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n)
(x : N) :
@[simp]
theorem
diffeomorph.symm_apply_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n)
(x : M) :
@[simp]
theorem
diffeomorph.symm_refl
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_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 : ℕ∞} :
(diffeomorph.refl I M n).symm = diffeomorph.refl I M n
@[simp]
theorem
diffeomorph.self_trans_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n) :
h.trans h.symm = diffeomorph.refl I M n
@[simp]
theorem
diffeomorph.symm_trans_self
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n) :
h.symm.trans h = diffeomorph.refl J N n
@[simp]
theorem
diffeomorph.symm_trans'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h₁ : diffeomorph I I' M M' n)
(h₂ : diffeomorph I' J M' N n) :
@[simp]
theorem
diffeomorph.symm_to_equiv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n) :
@[simp]
theorem
diffeomorph.to_equiv_coe_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n) :
theorem
diffeomorph.image_eq_preimage
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n)
(s : set M) :
theorem
diffeomorph.symm_image_eq_preimage
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n)
(s : set N) :
@[simp]
theorem
diffeomorph.range_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
{α : Sort u_3}
(h : diffeomorph I J M N n)
(f : α → M) :
@[simp]
theorem
diffeomorph.image_symm_image
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n)
(s : set N) :
@[simp]
theorem
diffeomorph.symm_image_image
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n)
(s : set M) :
def
diffeomorph.to_homeomorph
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n) :
M ≃ₜ N
A diffeomorphism is a homeomorphism.
Equations
- h.to_homeomorph = {to_equiv := h.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
diffeomorph.to_homeomorph_to_equiv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n) :
@[simp]
theorem
diffeomorph.symm_to_homeomorph
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n) :
@[simp]
theorem
diffeomorph.coe_to_homeomorph
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n) :
⇑(h.to_homeomorph) = ⇑h
@[simp]
theorem
diffeomorph.coe_to_homeomorph_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n) :
@[simp]
theorem
diffeomorph.cont_mdiff_within_at_comp_diffeomorph_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h : diffeomorph I J M N n)
(hn : 1 ≤ n) :
def
diffeomorph.prod_congr
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(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
- h₁.prod_congr h₂ = {to_equiv := h₁.to_equiv.prod_congr h₂.to_equiv, cont_mdiff_to_fun := _, cont_mdiff_inv_fun := _}
@[simp]
theorem
diffeomorph.prod_congr_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(h₁ : diffeomorph I I' M M' n)
(h₂ : diffeomorph J J' N N' n) :
def
diffeomorph.prod_comm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞) :
diffeomorph (I.prod J) (J.prod I) (M × N) (N × M) n
M × N is diffeomorphic to N × M.
Equations
- diffeomorph.prod_comm I J M N n = {to_equiv := equiv.prod_comm M N, cont_mdiff_to_fun := _, cont_mdiff_inv_fun := _}
@[simp]
theorem
diffeomorph.prod_comm_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞) :
(diffeomorph.prod_comm I J M N n).symm = diffeomorph.prod_comm J I N M n
@[simp]
theorem
diffeomorph.coe_prod_comm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞) :
⇑(diffeomorph.prod_comm I J M N n) = prod.swap
def
diffeomorph.prod_assoc
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞) :
(M × N) × N' is diffeomorphic to M × (N × N').
Equations
- diffeomorph.prod_assoc I J J' M N N' n = {to_equiv := equiv.prod_assoc M N N', cont_mdiff_to_fun := _, cont_mdiff_inv_fun := _}
theorem
diffeomorph.unique_mdiff_on_image_aux
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
[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) :
unique_mdiff_on J (⇑h '' s)
@[simp]
theorem
diffeomorph.unique_mdiff_on_image
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
[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} :
unique_mdiff_on J (⇑h '' s) ↔ unique_mdiff_on I s
@[simp]
theorem
diffeomorph.unique_mdiff_on_preimage
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
[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} :
unique_mdiff_on I (⇑h ⁻¹' s) ↔ unique_mdiff_on J s
@[simp]
theorem
diffeomorph.unique_diff_on_image
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
(h : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F n)
(hn : 1 ≤ n)
{s : set E} :
unique_diff_on 𝕜 (⇑h '' s) ↔ unique_diff_on 𝕜 s
@[simp]
theorem
diffeomorph.unique_diff_on_preimage
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
(h : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F n)
(hn : 1 ≤ n)
{s : set F} :
unique_diff_on 𝕜 (⇑h ⁻¹' s) ↔ unique_diff_on 𝕜 s
def
continuous_linear_equiv.to_diffeomorph
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
(e : E ≃L[𝕜] E') :
diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' ⊤
A continuous linear equivalence between normed spaces is a diffeomorphism.
Equations
- e.to_diffeomorph = {to_equiv := e.to_linear_equiv.to_equiv, cont_mdiff_to_fun := _, cont_mdiff_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.coe_to_diffeomorph
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
(e : E ≃L[𝕜] E') :
⇑(e.to_diffeomorph) = ⇑e
@[simp]
theorem
continuous_linear_equiv.symm_to_diffeomorph
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
(e : E ≃L[𝕜] E') :
@[simp]
theorem
continuous_linear_equiv.coe_to_diffeomorph_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
(e : E ≃L[𝕜] E') :
def
model_with_corners.trans_diffeomorph
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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' ⊤) :
model_with_corners 𝕜 E' H
Apply a diffeomorphism (e.g., a continuous linear equivalence) to the model vector space.
Equations
- I.trans_diffeomorph e = {to_local_equiv := I.to_local_equiv.trans e.to_equiv.to_local_equiv, source_eq := _, unique_diff' := _, continuous_to_fun := _, continuous_inv_fun := _}
Instances for model_with_corners.trans_diffeomorph
@[simp]
theorem
model_with_corners.coe_trans_diffeomorph
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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) :
⇑(ext_chart_at (I.trans_diffeomorph e) x) = ⇑e ∘ ⇑(ext_chart_at I x)
theorem
model_with_corners.coe_ext_chart_at_trans_diffeomorph_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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) :
⇑((ext_chart_at (I.trans_diffeomorph e) x).symm) = ⇑((ext_chart_at I x).symm) ∘ ⇑(e.symm)
theorem
model_with_corners.ext_chart_at_trans_diffeomorph_target
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_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) :
(ext_chart_at (I.trans_diffeomorph e) x).target = ⇑(e.symm) ⁻¹' (ext_chart_at I x).target
@[protected, instance]
def
diffeomorph.smooth_manifold_with_corners_trans_diffeomorph
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 ⊤)
[smooth_manifold_with_corners I M] :
def
diffeomorph.to_trans_diffeomorph
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_4}
[normed_add_comm_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 ⊤) :
diffeomorph I (I.trans_diffeomorph e) M M ⊤
The identity diffeomorphism between a manifold with model I and the same manifold
with model I.trans_diffeomorph e.
Equations
- diffeomorph.to_trans_diffeomorph I M e = {to_equiv := equiv.refl M, cont_mdiff_to_fun := _, cont_mdiff_inv_fun := _}
@[simp]
theorem
diffeomorph.cont_mdiff_within_at_trans_diffeomorph_right
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ⊤)
{f : M' → M}
{x : M'}
{s : set M'} :
cont_mdiff_within_at I' (I.trans_diffeomorph e) n f s x ↔ cont_mdiff_within_at I' I n f s x
@[simp]
theorem
diffeomorph.cont_mdiff_at_trans_diffeomorph_right
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ⊤)
{f : M' → M}
{x : M'} :
cont_mdiff_at I' (I.trans_diffeomorph e) n f x ↔ cont_mdiff_at I' I n f x
@[simp]
theorem
diffeomorph.cont_mdiff_on_trans_diffeomorph_right
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ⊤)
{f : M' → M}
{s : set M'} :
cont_mdiff_on I' (I.trans_diffeomorph e) n f s ↔ cont_mdiff_on I' I n f s
@[simp]
theorem
diffeomorph.cont_mdiff_trans_diffeomorph_right
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ⊤)
{f : M' → M} :
cont_mdiff I' (I.trans_diffeomorph e) n f ↔ cont_mdiff I' I n f
@[simp]
theorem
diffeomorph.smooth_trans_diffeomorph_right
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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} :
smooth I' (I.trans_diffeomorph e) f ↔ smooth I' I f
@[simp]
theorem
diffeomorph.cont_mdiff_within_at_trans_diffeomorph_left
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ⊤)
{f : M → M'}
{x : M}
{s : set M} :
cont_mdiff_within_at (I.trans_diffeomorph e) I' n f s x ↔ cont_mdiff_within_at I I' n f s x
@[simp]
theorem
diffeomorph.cont_mdiff_at_trans_diffeomorph_left
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ⊤)
{f : M → M'}
{x : M} :
cont_mdiff_at (I.trans_diffeomorph e) I' n f x ↔ cont_mdiff_at I I' n f x
@[simp]
theorem
diffeomorph.cont_mdiff_on_trans_diffeomorph_left
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ⊤)
{f : M → M'}
{s : set M} :
cont_mdiff_on (I.trans_diffeomorph e) I' n f s ↔ cont_mdiff_on I I' n f s
@[simp]
theorem
diffeomorph.cont_mdiff_trans_diffeomorph_left
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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 : ℕ∞}
(e : diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) E F ⊤)
{f : M → M'} :
cont_mdiff (I.trans_diffeomorph e) I' n f ↔ cont_mdiff I I' n f
@[simp]
theorem
diffeomorph.smooth_trans_diffeomorph_left
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F : Type u_4}
[normed_add_comm_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'} :
smooth (I.trans_diffeomorph e) I' f ↔ smooth I I' f