{L : Type u_1} →
  [inst : TopologicalSpace L] →
    [inst_1 : Min L] →
      {motive : ContinuousInf L → Sort u} →
        (t : ContinuousInf L) → ((continuous_inf : Continuous fun p => p.1 ⊓ p.2) → motive ⋯) → motive t