From 9d8ba939055398dc4f21d40df61fe8419bafe164 Mon Sep 17 00:00:00 2001
From: Hannah Scholz <hannah@scholzbande.de>
Date: Thu, 24 Oct 2024 19:28:37 +0000
Subject: [PATCH] feat: `T2Space` is `Antitone` (#18188)

---
 Mathlib/Topology/Separation.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
index a99e1b615e460..284f7ef7efa3c 100644
--- a/Mathlib/Topology/Separation.lean
+++ b/Mathlib/Topology/Separation.lean
@@ -1892,6 +1892,10 @@ theorem not_preirreducible_nontrivial_t2 (X) [TopologicalSpace X] [Preirreducibl
     [Nontrivial X] [T2Space X] : False :=
   (PreirreducibleSpace.isPreirreducible_univ (X := X)).subsingleton.not_nontrivial nontrivial_univ
 
+theorem t2Space_antitone {X : Type*} : Antitone (@T2Space X) :=
+  fun inst₁ inst₂ h_top h_t2 ↦ @T2Space.of_injective_continuous _ _ inst₁ inst₂
+    h_t2 _ Function.injective_id <| continuous_id_of_le h_top
+
 end Separation
 
 section RegularSpace