Theorems · Definition · general topology

IsSpectralMap.casesOn

{α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {f : α → β} →
          {motive : IsSpectralMap f → Sort u} →
            (t : IsSpectralMap f) →
              ((toContinuous : Continuous f) →
                  (isCompact_preimage_of_isOpen : ∀ ⦃s : Set β⦄, IsOpen s → IsCompact s → IsCompact (f ⁻¹' s)) →
                    motive ⋯) →
                motive t

Defined in

Mathlib.Topology.Spectral.Hom

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace