wip tinkering

Mathlib/Geometry/Manifold/Bordisms.lean

@@ -216,6 +216,15 @@ def trivial (hequiv : H ≃ₜ EuclideanSpace ℝ (Fin n)) [h: Fact (finrank ℝ
   f := fun _ ↦ PUnit.unit
   hf := continuous_const
 
+variable (α : Type*)
+#synth TopologicalSpace (WithLp 2   α)
+
+def WithLp.prodEquivSum (α β 𝕜 : Type*) [NontriviallyNormedField 𝕜] :
+    (WithLp 2 (PiLp 2 (fun _ : α ↦ 𝕜))) × (EuclideanSpace 𝕜 β) ≃ₜ EuclideanSpace 𝕜 (α ⊕ β) where
+  toEquiv := (Equiv.sumArrowEquivProdArrow α β 𝕜).symm
+  continuous_toFun := sorry
+  continuous_invFun := sorry
+
 def EuclideanSpace.prodEquivSum (α β 𝕜 : Type*) [NontriviallyNormedField 𝕜] :
     (EuclideanSpace 𝕜 α) × (EuclideanSpace 𝕜 β) ≃ₜ EuclideanSpace 𝕜 (α ⊕ β) where
   toEquiv := (Equiv.sumArrowEquivProdArrow α β 𝕜).symm
@@ -262,6 +271,7 @@ instance {n : ℕ} (s t : SingularNManifold X n k) :
   haveI := ChartedSpace.comp (EuclideanSpace ℝ (Fin n)) t.H t.M
   infer_instance
 
+-- missing: if M is a manifold w.r.t. I over (E, H), this transfer across a homeo
 instance {n : ℕ} (s t : SingularNManifold X n k) : IsManifold (𝓡 n) k (s.M ⊕ t.M) := sorry
 
 /-- The disjoint union of two singular `n`-manifolds on `X` is a singular `n`-manifold on `X`. -/