Diffeomorphisms

Diffeomorphisms between diffeological spaces. Mostly copied from Mathlib.Geometry.Manifold.Diffeomorph.

structure DDiffeomorph (X : Type u_1) (Y : Type u_2) [DiffeologicalSpace X] [DiffeologicalSpace Y] extends X ≃ Y : Type (max u_1 u_2)

• toFun : X → Y
• invFun : Y → X
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• dsmooth_toFun : DSmooth self.toFun
• dsmooth_invFun : DSmooth self.invFun

def «term_ᵈ≃_» : Lean.TrailingParserDescr

Equations

• «term_ᵈ≃_» = Lean.ParserDescr.trailingNode `«term_ᵈ≃_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᵈ≃ ") (Lean.ParserDescr.cat `term 26))

theorem DDiffeomorph.toEquiv_injective {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] : Function.Injective toEquiv

@[implicit_reducible]

instance DDiffeomorph.instEquivLike {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] : EquivLike (X ᵈ≃ Y) X Y

Equations

• DDiffeomorph.instEquivLike = { coe := fun (Φ : X ᵈ≃ Y) => ⇑Φ.toEquiv, inv := fun (Φ : X ᵈ≃ Y) => ⇑Φ.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

theorem DDiffeomorph.continuous {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : Continuous ⇑h

theorem DDiffeomorph.continuous' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) : Continuous ⇑h

theorem DDiffeomorph.dsmooth {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : DSmooth ⇑h

theorem DDiffeomorph.isInduction {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : IsInduction ⇑h

theorem DDiffeomorph.isOpenInduction {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : IsOpenInduction ⇑h

theorem DDiffeomorph.isSubduction {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : IsSubduction ⇑h

@[simp]

theorem DDiffeomorph.coe_toEquiv {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : ⇑h.toEquiv = ⇑h

@[simp]

theorem DDiffeomorph.toEquiv_inj {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {h h' : X ᵈ≃ Y} : h.toEquiv = h'.toEquiv ↔ h = h'

theorem DDiffeomorph.coeFn_injective {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] : Function.Injective DFunLike.coe

theorem DDiffeomorph.bijective {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : Function.Bijective ⇑h

theorem DDiffeomorph.injective {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : Function.Injective ⇑h

theorem DDiffeomorph.surjective {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : Function.Surjective ⇑h

theorem DDiffeomorph.ext {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {h h' : X ᵈ≃ Y} (heq : ∀ (x : X), h x = h' x) : h = h'

theorem DDiffeomorph.ext_iff {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {h h' : X ᵈ≃ Y} : h = h' ↔ ∀ (x : X), h x = h' x

def DDiffeomorph.refl (X : Type u_4) [DiffeologicalSpace X] : X ᵈ≃ X

Identity map as a diffeomorphism.

Equations

• DDiffeomorph.refl X = { toEquiv := Equiv.refl X, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

@[simp]

theorem DDiffeomorph.refl_toEquiv {X : Type u_1} [DiffeologicalSpace X] : (DDiffeomorph.refl X).toEquiv = Equiv.refl X

@[simp]

theorem DDiffeomorph.coe_refl {X : Type u_1} [DiffeologicalSpace X] : ⇑(DDiffeomorph.refl X) = id

def DDiffeomorph.trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (h₁ : X ᵈ≃ Y) (h₂ : Y ᵈ≃ Z) : X ᵈ≃ Z

Composition of diffeomorphisms.

Equations

• h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

@[simp]

theorem DDiffeomorph.trans_refl {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : h.trans (DDiffeomorph.refl Y) = h

@[simp]

theorem DDiffeomorph.refl_trans {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : (DDiffeomorph.refl X).trans h = h

@[simp]

theorem DDiffeomorph.coe_trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (h₁ : X ᵈ≃ Y) (h₂ : Y ᵈ≃ Z) : ⇑(h₁.trans h₂) = ⇑h₂ ∘ ⇑h₁

def DDiffeomorph.symm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : Y ᵈ≃ X

Inverse of a diffeomorphism.

Equations

• h.symm = { toEquiv := h.symm, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

@[simp]

theorem DDiffeomorph.apply_symm_apply {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (y : Y) : h (h.symm y) = y

@[simp]

theorem DDiffeomorph.symm_apply_apply {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (x : X) : h.symm (h x) = x

@[simp]

theorem DDiffeomorph.symm_refl {X : Type u_1} [DiffeologicalSpace X] : (DDiffeomorph.refl X).symm = DDiffeomorph.refl X

@[simp]

theorem DDiffeomorph.self_trans_symm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : h.trans h.symm = DDiffeomorph.refl X

@[simp]

theorem DDiffeomorph.symm_trans_self {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : h.symm.trans h = DDiffeomorph.refl Y

@[simp]

theorem DDiffeomorph.symm_trans' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (h₁ : X ᵈ≃ Y) (h₂ : Y ᵈ≃ Z) : (h₁.trans h₂).symm = h₂.symm.trans h₁.symm

@[simp]

theorem DDiffeomorph.symm_toEquiv {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : h.symm.toEquiv = h.symm

@[simp]

theorem DDiffeomorph.toEquiv_coe_symm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : ⇑h.symm = ⇑h.symm

theorem DDiffeomorph.image_eq_preimage {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (s : Set X) : ⇑h '' s = ⇑h.symm ⁻¹' s

theorem DDiffeomorph.symm_image_eq_preimage {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (s : Set Y) : ⇑h.symm '' s = ⇑h ⁻¹' s

@[simp]

theorem DDiffeomorph.range_comp {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {α : Type u_4} (h : X ᵈ≃ Y) (f : α → X) : Set.range (⇑h ∘ f) = ⇑h.symm ⁻¹' Set.range f

@[simp]

theorem DDiffeomorph.image_symm_image {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (s : Set Y) : ⇑h '' (⇑h.symm '' s) = s

@[simp]

theorem DDiffeomorph.symm_image_image {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (s : Set X) : ⇑h.symm '' (⇑h '' s) = s

noncomputable def DDiffeomorph.ofIsInduction {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {f : X → Y} (hf : IsInduction f) : X ᵈ≃ ↑(Set.range f)

An induction is a diffeomorphism onto its image.

Equations

• DDiffeomorph.ofIsInduction hf = { toEquiv := Equiv.ofInjective f ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

def DDiffeomorph.toHomeomorph {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : X ≃ₜ Y

A diffeomorphism is a homeomorphism with respect to the D-topologies.

Equations

• h.toHomeomorph = { toEquiv := h.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem DDiffeomorph.toHomeomorph_toEquiv {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : h.toHomeomorph.toEquiv = h.toEquiv

@[simp]

theorem DDiffeomorph.symm_toHomeomorph {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : h.symm.toHomeomorph = h.toHomeomorph.symm

@[simp]

theorem DDiffeomorph.coe_toHomeomorph {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : ⇑h.toHomeomorph = ⇑h

@[simp]

theorem DDiffeomorph.coe_toHomeomorph_symm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) : ⇑h.toHomeomorph.symm = ⇑h.symm

def DDiffeomorph.toHomeomorph' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) : X ≃ₜ Y

A diffeomorphism between spaces that are equipped with the D-topologies is also a homeoomorphism.

Equations

• h.toHomeomorph' = { toEquiv := h.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem DDiffeomorph.toHomeomorph_toEquiv' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) : h.toHomeomorph'.toEquiv = h.toEquiv

@[simp]

theorem DDiffeomorph.symm_toHomeomorph' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) : h.symm.toHomeomorph' = h.toHomeomorph'.symm

@[simp]

theorem DDiffeomorph.coe_toHomeomorph' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) : ⇑h.toHomeomorph' = ⇑h

@[simp]

theorem DDiffeomorph.coe_toHomeomorph_symm' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) : ⇑h.toHomeomorph'.symm = ⇑h.symm

theorem DDiffeomorph.dTopCompatible {X : Type u_4} {Y : Type u_5} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] (e : X ᵈ≃ Y) (h : IsHomeomorph ⇑e) [DTopCompatible X] : DTopCompatible Y

If a diffeomorphism between diffeological spaces equipped with topologies is also a homeomorphism and the topology on the domain agrees with the D-topology, then the topology on the codomain does as well.

@[simp]

theorem DDiffeomorph.dsmooth_comp_ddiffeomorph_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (h : X ᵈ≃ Y) {f : Y → Z} : DSmooth (f ∘ ⇑h) ↔ DSmooth f

@[simp]

theorem DDiffeomorph.dsmooth_ddiffeomorph_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (h : X ᵈ≃ Y) {f : Z → X} : DSmooth (⇑h ∘ f) ↔ DSmooth f

theorem IsInduction.dsmooth_comp_iff_dsmooth_restrict {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : X → Y} (hf : IsInduction f) {g : Y → Z} : DSmooth (g ∘ f) ↔ DSmooth ((Set.range f).restrict g)

For any induction f, g ∘ f is smooth iff g is smooth on Set.range f. TODO: move to a more fitting location

instance DDiffeomorph.instContinuousMapClass {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] : DSmoothMapClass (X ᵈ≃ Y) X Y

@[reducible, inline]

abbrev DDiffeomorph.toDSmoothMap {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (d : X ᵈ≃ Y) : DSmoothMap X Y

Equations

• d.toDSmoothMap = ↑d

@[simp]

theorem DDiffeomorph.toDSmoothMap_refl {X : Type u_1} [DiffeologicalSpace X] : ↑(DDiffeomorph.refl X) = DSmoothMap.id X

@[simp]

theorem DDiffeomorph.toDSmoothMap_trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (f : X ᵈ≃ Y) (g : Y ᵈ≃ Z) : ↑(f.trans g) = (↑g).comp ↑f

@[simp]

theorem DDiffeomorph.symm_comp_toDSmoothMap {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : X ᵈ≃ Y) : (↑f.symm).comp ↑f = DSmoothMap.id X

Left inverse to a continuous map from a homeomorphism, mirroring Equiv.symm_comp_self.

@[simp]

theorem DDiffeomorph.toDSmoothMap_comp_symm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : X ᵈ≃ Y) : (↑f).comp ↑f.symm = DSmoothMap.id Y

Right inverse to a continuous map from a homeomorphism, mirroring Equiv.self_comp_symm.

noncomputable def DDiffeomorph.univBall {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [DiffeologicalSpace E] [ContDiffCompatible E] (x : E) {r : ℝ} (hr : r > 0) : E ᵈ≃ ↑(Metric.ball x r)

Inner product spaces are diffeomorphic to open balls in them.

Equations

• One or more equations did not get rendered due to their size.

theorem DDiffeomorph.coe_univBall_zero {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [DiffeologicalSpace E] [ContDiffCompatible E] (x : E) {r : ℝ} (hr : r > 0) : ↑((univBall x hr) 0) = x

def DDiffeomorph.Set.univ (X : Type u_4) [DiffeologicalSpace X] : ↑_root_.Set.univ ᵈ≃ X

Set.univ X is diffeomorphic to X.

Equations

• DDiffeomorph.Set.univ X = { toEquiv := Equiv.Set.univ X, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

@[simp]

theorem DDiffeomorph.Set.univ_invFun_coe (X : Type u_4) [DiffeologicalSpace X] (a : X) : ↑((univ X).invFun a) = a

@[simp]

theorem DDiffeomorph.Set.univ_toFun (X : Type u_4) [DiffeologicalSpace X] : ⇑(univ X) = Subtype.val

def DDiffeomorph.Set.nested {X : Type u_1} [DiffeologicalSpace X] {u : Set X} (v : Set ↑u) : ↑v ᵈ≃ ↑(Subtype.val '' v)

Equations

• One or more equations did not get rendered due to their size.

def DDiffeomorph.restrict {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (d : X ᵈ≃ Y) (u : Set X) : ↑u ᵈ≃ ↑(⇑d.symm ⁻¹' u)

Equations

• d.restrict u = { toFun := Set.MapsTo.restrict (⇑d) u (⇑d.symm ⁻¹' u) ⋯, invFun := u.restrictPreimage ⇑d.symm, left_inv := ⋯, right_inv := ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

def DDiffeomorph.restrictPreimage {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (d : X ᵈ≃ Y) (u : Set Y) : ↑(⇑d ⁻¹' u) ᵈ≃ ↑u

Equations

• One or more equations did not get rendered due to their size.

def DDiffeomorph.quotient_bot (X : Type u_4) [DiffeologicalSpace X] : Quotient ⊥ ᵈ≃ X

The quotient of X by the identity relation is diffeomorphic to X.

Equations

• DDiffeomorph.quotient_bot X = { toFun := Quotient.lift id ⋯, invFun := Quotient.mk', left_inv := ⋯, right_inv := ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

@[simp]

theorem DDiffeomorph.quotient_bot_invFun (X : Type u_4) [DiffeologicalSpace X] : (quotient_bot X).invFun = Quotient.mk'

@[simp]

theorem DDiffeomorph.quotient_bot_toFun (X : Type u_4) [DiffeologicalSpace X] : ⇑(quotient_bot X) = Quotient.lift id ⋯

def DDiffeomorph.prodComm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] : X × Y ᵈ≃ Y × X

Equations

• DDiffeomorph.prodComm = { toFun := Prod.swap, invFun := Prod.swap, left_inv := ⋯, right_inv := ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

def DDiffeomorph.curry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] : DSmoothMap (X × Y) Z ᵈ≃ DSmoothMap X (DSmoothMap Y Z)

The currying diffeomorphism DSmoothMap (X × Y) Z ᵈ≃ DSmoothMap X (DSmoothMap Y Z).

Equations

• DDiffeomorph.curry = { toFun := DSmoothMap.curry, invFun := DSmoothMap.uncurry, left_inv := ⋯, right_inv := ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

def DDiffeomorph.comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (d : Y ᵈ≃ Z) : DSmoothMap X Y ᵈ≃ DSmoothMap X Z

Postcomposition with d : Y ᵈ≃ Z as a diffeomorphism DSmoothMap X Y ᵈ≃ DSmoothMap X Z.

Equations

• One or more equations did not get rendered due to their size.

def DDiffeomorph.comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (d : X ᵈ≃ Y) : DSmoothMap Y Z ᵈ≃ DSmoothMap X Z

Precomposition with d : X ᵈ≃ Y as a diffeomorphism DSmoothMap Y Z ᵈ≃ DSmoothMap X Z.

Equations

• d.comp_right = { toFun := fun (f : DSmoothMap Y Z) => f.comp ↑d, invFun := fun (f : DSmoothMap X Z) => f.comp ↑d.symm, left_inv := ⋯, right_inv := ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

def ContinuousLinearEquiv.toDDiffeomorph {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [DiffeologicalSpace E] [ContDiffCompatible E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [DiffeologicalSpace E'] [ContDiffCompatible E'] (e : E ≃L[ℝ] E') : E ᵈ≃ E'

A continuous linear equivalence between (for now just finite-dimensional) normed spaces is a diffeomorphism.

Equations

• e.toDDiffeomorph = { toEquiv := e.toEquiv, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.coe_toDDiffeomorph {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [DiffeologicalSpace E] [ContDiffCompatible E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [DiffeologicalSpace E'] [ContDiffCompatible E'] (e : E ≃L[ℝ] E') : ⇑e.toDDiffeomorph = ⇑e

@[simp]

theorem ContinuousLinearEquiv.symm_toDDiffeomorph {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [DiffeologicalSpace E] [ContDiffCompatible E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [DiffeologicalSpace E'] [ContDiffCompatible E'] (e : E ≃L[ℝ] E') : e.symm.toDDiffeomorph = e.toDDiffeomorph.symm

@[simp]

theorem ContinuousLinearEquiv.coe_toDDiffeomorph_symm {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [DiffeologicalSpace E] [ContDiffCompatible E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [DiffeologicalSpace E'] [ContDiffCompatible E'] (e : E ≃L[ℝ] E') : ⇑e.toDDiffeomorph.symm = ⇑e.symm