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