feat: port Topology.Order (#1843)

Author: urkud

Mathlib.lean

@@ -914,6 +914,7 @@ import Mathlib.Topology.Bornology.Constructions
 import Mathlib.Topology.Bornology.Hom
 import Mathlib.Topology.LocallyFinite
 import Mathlib.Topology.NhdsSet
+import Mathlib.Topology.Order
 import Mathlib.Util.AtomM
 import Mathlib.Util.Export
 import Mathlib.Util.IncludeStr

Mathlib/Topology/Basic.lean

@@ -1569,6 +1569,11 @@ structure Continuous (f : α → β) : Prop where
   is_open_preimage : ∀ s, IsOpen s → IsOpen (f ⁻¹' s)
 #align continuous Continuous
 
+set_option quotPrecheck false in
+/-- Notation for `Continuous` with respect to a non-standard topologies. -/
+scoped[Topology] notation (name := Continuous_of) "Continuous[" t₁ ", " t₂ "]" =>
+  @Continuous _ _ t₁ t₂
+
 theorem continuous_def {_ : TopologicalSpace α} {_ : TopologicalSpace β} {f : α → β} :
     Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) :=
   ⟨fun hf s hs => hf.is_open_preimage s hs, fun h => ⟨h⟩⟩