refactor(Probability/Kernel/CondCdf): mv some theorems (#10036)

Co-authored-by: Moritz Firsching <[email protected]>

Mathlib/Logic/Encodable/Basic.lean

@@ -655,7 +655,11 @@ theorem rel_sequence {r : β → β → Prop} {f : α → β} (hf : Directed r f
   exact (Classical.choose_spec (hf _ a)).2
 #align directed.rel_sequence Directed.rel_sequence
 
-variable [Preorder β] {f : α → β} (hf : Directed (· ≤ ·) f)
+variable [Preorder β] {f : α → β}
+
+section
+
+variable (hf : Directed (· ≤ ·) f)
 
 theorem sequence_mono : Monotone (f ∘ hf.sequence f) :=
   monotone_nat_of_le_succ <| hf.sequence_mono_nat
@@ -665,6 +669,22 @@ theorem le_sequence (a : α) : f a ≤ f (hf.sequence f (encode a + 1)) :=
   hf.rel_sequence a
 #align directed.le_sequence Directed.le_sequence
 
+end
+
+section
+
+variable (hf : Directed (· ≥ ·) f)
+
+theorem sequence_anti : Antitone (f ∘ hf.sequence f) :=
+  antitone_nat_of_succ_le <| hf.sequence_mono_nat
+#align directed.sequence_anti Directed.sequence_anti
+
+theorem sequence_le (a : α) : f (hf.sequence f (Encodable.encode a + 1)) ≤ f a :=
+  hf.rel_sequence a
+#align directed.sequence_le Directed.sequence_le
+
+end
+
 end Directed
 
 section Quotient

Mathlib/Probability/Kernel/CondCdf.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
+import Mathlib.Logic.Encodable.Basic
 import Mathlib.Data.Set.Lattice
 import Mathlib.MeasureTheory.Measure.Stieltjes
 import Mathlib.MeasureTheory.Decomposition.RadonNikodym
@@ -52,21 +53,6 @@ section AuxLemmasToBeMoved
 
 variable {α β ι : Type*}
 
-namespace Directed
-
--- todo after the port: move this to logic.encodable.basic near sequence_mono
-variable [Encodable α] [Inhabited α] [Preorder β] {f : α → β} (hf : Directed (· ≥ ·) f)
-
-theorem sequence_anti : Antitone (f ∘ hf.sequence f) :=
-  antitone_nat_of_succ_le <| hf.sequence_mono_nat
-#align directed.sequence_anti Directed.sequence_anti
-
-theorem sequence_le (a : α) : f (hf.sequence f (Encodable.encode a + 1)) ≤ f a :=
-  hf.rel_sequence a
-#align directed.sequence_le Directed.sequence_le
-
-end Directed
-
 theorem Real.iUnion_Iic_rat : ⋃ r : ℚ, Iic (r : ℝ) = univ := by
   ext1 x
   simp only [mem_iUnion, mem_Iic, mem_univ, iff_true_iff]