rw [this]
X : Type
T : Topology X
this : Set.univ = ⋂ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen Set.univ
X : Type
T : Topology X
this : Set.univ = ⋂ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen (⋂ i, Empty.rec (fun x => Set X) i)