Theorems · Theorem · global analysis

writtenInExtChart_prod

Deprecated since 2026-02-18Use writtenInExtChartAt_prod instead.

∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] {I : ModelWithCorners 𝕜 E H}
  [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] [inst_7 : TopologicalSpace H']
  [inst_8 : TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} [inst_9 : ChartedSpace H M]
  [inst_10 : ChartedSpace H' M'] {G : Type u_8} {G' : Type u_9} {F : Type u_10} {F' : Type u_11} {N : Type u_12}
  {N' : Type u_13} [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] [inst_13 : NormedAddCommGroup F']
  [inst_14 : NormedSpace 𝕜 F'] [inst_15 : TopologicalSpace G] [inst_16 : TopologicalSpace N]
  [inst_17 : TopologicalSpace G'] [inst_18 : TopologicalSpace N'] {J : ModelWithCorners 𝕜 F G}
  {J' : ModelWithCorners 𝕜 F' G'} [inst_19 : ChartedSpace G N] [inst_20 : ChartedSpace G' N'] {f : M → N} {g : M' → N'}
  {x : M} {x' : M'},
  writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) =
    Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g)

Alias of writtenInExtChartAt_prod.

Defined in

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Cited by

0 results in Mathlib

Foundations

Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceChartedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceChartedSpace