Theorems · Definition · general topology

ZeroAtInftyContinuousMapClass.casesOn

{F : Type u_2} →
  {α : Type u_3} →
    {β : Type u_4} →
      [inst : TopologicalSpace α] →
        [inst_1 : Zero β] →
          [inst_2 : TopologicalSpace β] →
            [inst_3 : FunLike F α β] →
              {motive : ZeroAtInftyContinuousMapClass F α β → Sort u} →
                (t : ZeroAtInftyContinuousMapClass F α β) →
                  ([toContinuousMapClass : ContinuousMapClass F α β] →
                      (zero_at_infty : ∀ (f : F), Filter.Tendsto (⇑f) (Filter.cocompact α) (nhds 0)) → motive ⋯) →
                    motive t

Defined in

Mathlib.Topology.ContinuousMap.ZeroAtInfty

Cited by

0 results in Mathlib

Foundations

Depth 53 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceZeroTopologicalSpaceFunLike