Theorems · Definition · general topology

Topology.ContinuousMapGeneratedBy.casesOn

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

Defined in

Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace