Theorems · Definition · general topology

Topology.ContinuousMapGeneratedBy.mk.noConfusion

{ι : Type t} →
  {X : ι → Type u} →
    {inst : (i : ι) → TopologicalSpace (X i)} →
      {Y : Type v} →
        {inst_1 : TopologicalSpace Y} →
          {Z : Type v'} →
            {inst_2 : TopologicalSpace Z} →
              {P : Sort u_1} →
                {toFun : Y → Z} →
                  {prop : Topology.ContinuousGeneratedBy X toFun} →
                    {toFun' : Y → Z} →
                      {prop' : Topology.ContinuousGeneratedBy X toFun'} →
                        { toFun := toFun, prop := prop } = { toFun := toFun', prop := prop' } → (toFun ≍ toFun' → P) → P

Defined in

Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Cited by

1 results in Mathlib

Foundations

Depth 20 from the axioms · uses no axioms