Theorems · Definition · general topology

CompletelyRegularSpace.casesOn

{X : Type u} →
  [inst : TopologicalSpace X] →
    {motive : CompletelyRegularSpace X → Sort u_1} →
      (t : CompletelyRegularSpace X) →
        ((completely_regular :
              ∀ (x : X) (K : Set X), IsClosed K → x ∉ K → ∃ f, Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K) →
            motive ⋯) →
          motive t

Defined in

Mathlib.Topology.Separation.CompletelyRegular

Cited by

1 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace