From f09a6b338a8e703df638ab7c17545151004191bc Mon Sep 17 00:00:00 2001
From: Columbus240 <8899730+Columbus240@users.noreply.github.com>
Date: Tue, 6 Aug 2024 16:56:25 +0200
Subject: [PATCH] Prove that `Subnet` is reflexive and transitive

---
 theories/Topology/Nets.v | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/theories/Topology/Nets.v b/theories/Topology/Nets.v
index 64fe42f..e5b529b 100644
--- a/theories/Topology/Nets.v
+++ b/theories/Topology/Nets.v
@@ -18,6 +18,36 @@ Definition Subnet {I : DirectedSet} {X : Type}
     (forall j : DS_set J,
         y j = x (h j)).
 
+Lemma Subnet_refl {I : DirectedSet} {X : Type} (x : Net I X) :
+  Subnet x x.
+Proof.
+  exists id. split; [|split].
+  - tauto.
+  - intros i. exists i. split.
+    + apply I.
+    + exists i; reflexivity.
+  - reflexivity.
+Qed.
+
+Lemma Subnet_trans {I J K : DirectedSet} {X : Type}
+  (x : Net I X) (y : Net J X) (z : Net K X) :
+  Subnet x y -> Subnet y z -> Subnet x z.
+Proof.
+  intros [f [Hf1 [Hf2 Hf3]]]
+         [g [Hg1 [Hg2 Hg3]]].
+  exists (compose f g). split; [|split].
+  - intros j1 j2 Hjj. apply Hf1, Hg1, Hjj.
+  - intros i.
+    specialize (Hf2 i) as [j0 [Hij [j Hj]]].
+    subst j0.
+    specialize (Hg2 j) as [k0 [Hjk [k Hk]]].
+    subst k0.
+    exists (f (g k)). split.
+    + apply preord_trans with (f j); auto. apply I.
+    + exists k. reflexivity.
+  - intros k. rewrite Hg3, Hf3. reflexivity.
+Qed.
+
 Section Net.
 Variable I:DirectedSet.
 Variable X:TopologicalSpace.