Theorems · Theorem · global analysis

contMDiff_tangentBundleModelSpaceHomeomorph

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H},
  ContMDiff I.tangent (I.prod (modelWithCornersSelf 𝕜 E)) n ⇑(tangentBundleModelSpaceHomeomorph I)

Defined in: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Cited by: 1 results in Mathlib
Foundations: Depth 219 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NontriviallyNormedField NormedAddCommGroup NormedSpace TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites49

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
TopologicalSpacestatement and proof · cited by 24,529
NormedAddCommGroupstatement and proof · cited by 15,752
NormedSpacestatement and proof · cited by 12,499
Top.topstatement · cited by 9,680
NontriviallyNormedFieldstatement and proof · cited by 8,742
ENatstatement and proof · cited by 4,985
Set.preimageproof · cited by 4,946
Set.rangeproof · cited by 4,705
Set.univproof · cited by 3,945
WithTopstatement and proof · cited by 3,754
ModelWithCornersstatement and proof · cited by 2,462

Cited by1

Results whose statement or proof uses this declaration.

contMDiff_snd_tangentBundle_modelSpaceproof · cited by 2