Theorems · Theorem · global analysis

ModelWithCorners.mk.inj

∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {E : Type u_2} {inst_1 : NormedAddCommGroup E}
  {inst_2 : NormedSpace 𝕜 E} {H : Type u_3} {inst_3 : TopologicalSpace H} {toPartialEquiv : PartialEquiv H E}
  {source_eq : toPartialEquiv.source = Set.univ}
  {convex_range' :
    if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑toPartialEquiv) else Set.range ↑toPartialEquiv = Set.univ}
  {nonempty_interior' : (interior (Set.range ↑toPartialEquiv)).Nonempty}
  {continuous_toFun : autoParam (Continuous ↑toPartialEquiv) ModelWithCorners.continuous_toFun._autoParam}
  {continuous_invFun : autoParam (Continuous toPartialEquiv.invFun) ModelWithCorners.continuous_invFun._autoParam}
  {toPartialEquiv_1 : PartialEquiv H E} {source_eq_1 : toPartialEquiv_1.source = Set.univ}
  {convex_range'_1 :
    if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑toPartialEquiv_1)
    else Set.range ↑toPartialEquiv_1 = Set.univ}
  {nonempty_interior'_1 : (interior (Set.range ↑toPartialEquiv_1)).Nonempty}
  {continuous_toFun_1 : autoParam (Continuous ↑toPartialEquiv_1) ModelWithCorners.continuous_toFun._autoParam}
  {continuous_invFun_1 : autoParam (Continuous toPartialEquiv_1.invFun) ModelWithCorners.continuous_invFun._autoParam},
  { toPartialEquiv := toPartialEquiv, source_eq := source_eq, convex_range' := convex_range',
        nonempty_interior' := nonempty_interior', continuous_toFun := continuous_toFun,
        continuous_invFun := continuous_invFun } =
      { toPartialEquiv := toPartialEquiv_1, source_eq := source_eq_1, convex_range' := convex_range'_1,
        nonempty_interior' := nonempty_interior'_1, continuous_toFun := continuous_toFun_1,
        continuous_invFun := continuous_invFun_1 } →
    toPartialEquiv = toPartialEquiv_1

Defined in

Mathlib.Geometry.Manifold.IsManifold.Basic

Cited by

1 results in Mathlib

Foundations

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