ext V
X Y : Type
f : X → Y
t : Set (Topology X)
⊢ f⁎ (Sup t) = Sup (f⁎ '' t)
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ Topology.isOpen (f⁎ (Sup t)) V ↔ Topology.isOpen (Sup (f⁎ '' t)) V