Theorems · Definition · general topology

Topology.ContinuousMapGeneratedBy.noConfusion

{P : Sort u_1} →
  {ι : Type t} →
    {X : ι → Type u} →
      {inst : (i : ι) → TopologicalSpace (X i)} →
        {Y : Type v} →
          {inst_1 : TopologicalSpace Y} →
            {Z : Type v'} →
              {inst_2 : TopologicalSpace Z} →
                {t : Topology.ContinuousMapGeneratedBy X Y Z} →
                  {ι' : Type t} →
                    {X' : ι' → Type u} →
                      {inst' : (i : ι') → TopologicalSpace (X' i)} →
                        {Y' : Type v} →
                          {inst'_1 : TopologicalSpace Y'} →
                            {Z' : Type v'} →
                              {inst'_2 : TopologicalSpace Z'} →
                                {t' : Topology.ContinuousMapGeneratedBy X' Y' Z'} →
                                  ι = ι' →
                                    X ≍ X' →
                                      inst ≍ inst' →
                                        Y = Y' →
                                          inst_1 ≍ inst'_1 →
                                            Z = Z' →
                                              inst_2 ≍ inst'_2 →
                                                t ≍ t' → Topology.ContinuousMapGeneratedBy.noConfusionType P t t'

Defined in

Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses no axioms