Theorems · Definition · general topology

Topology.IsLower.casesOn

{α : Type u_3} →
  [t : TopologicalSpace α] →
    [inst : Preorder α] →
      {motive : Topology.IsLower α → Sort u} →
        (t_1 : Topology.IsLower α) → ((topology_eq_lowerTopology : t = Topology.lower α) → motive ⋯) → motive t_1

Defined in

Mathlib.Topology.Order.LowerUpperTopology

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

TopologicalSpacePreorder