ext V
X Y Z : Type
f : X → Y
g : Y → Z
T : Topology X
⊢ g⁎ (f⁎ T) = (g ∘ f)⁎ T
case isOpen.h.a
X Y Z : Type
f : X → Y
g : Y → Z
T : Topology X
V : Set Z
⊢ Topology.isOpen (g⁎ (f⁎ T)) V ↔ Topology.isOpen ((g ∘ f)⁎ T) V