no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : TopologicalSpace β
f g : β → α
hf : Continuous f
hg : Continuous g
⊢ IsOpen {b | f b < g b}
simpa only [lt_iff_not_le] using (isClosed_le hg hf).isOpen_compl