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