Theorems · Definition · global analysis

ModelWithCorners.mk.noConfusion

{𝕜 : 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} →
              {P : Sort u} →
                {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' : 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 := toPartialEquiv, source_eq := source_eq,
                                              convex_range' := convex_range', nonempty_interior' := nonempty_interior',
                                              continuous_toFun := continuous_toFun,
                                              continuous_invFun := continuous_invFun } =
                                            { toPartialEquiv := toPartialEquiv', source_eq := source_eq',
                                              convex_range' := convex_range'',
                                              nonempty_interior' := nonempty_interior'',
                                              continuous_toFun := continuous_toFun',
                                              continuous_invFun := continuous_invFun' } →
                                          (toPartialEquiv ≍ toPartialEquiv' → P) → P

Defined in

Mathlib.Geometry.Manifold.IsManifold.Basic

Cited by

1 results in Mathlib

Foundations

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