Theorems · Theorem · global analysis

Manifold.IsImmersionAtOfComplement.equiv.congr_simp

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I I_1 : ModelWithCorners 𝕜 E H}
  (e_I : I = I_1) {J J_1 : ModelWithCorners 𝕜 E'' G} (e_J : J = J_1) {M : Type u_11} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N]
  {n n_1 : WithTop ℕ∞} (e_n : n = n_1) {f f_1 : M → N} (e_f : f = f_1) {x x_1 : M} (e_x : x = x_1)
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), h.equiv = ⋯.equiv

Defined in

Mathlib.Geometry.Manifold.Immersion

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpace