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

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