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

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