Theorems · Definition · general topology

Ctop.Realizer.casesOn

{α : Type u_6} →
  [T : TopologicalSpace α] →
    {motive : Ctop.Realizer α → Sort u} →
      (t : Ctop.Realizer α) →
        ((σ : Type u_5) → (F : Ctop α σ) → (eq : F.toTopsp = T) → motive { σ := σ, F := F, eq := eq }) → motive t

Defined in

Mathlib.Data.Analysis.Topology

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

TopologicalSpace