rename

Author: gaetanserre

Mathlib/Probability/Kernel/Category/SFinKer.lean

@@ -241,38 +241,38 @@ instance : CopyDiscardCategory SFinKer.{u} where
     rw [Kernel.id_map (by fun_prop)]
     simp [Kernel.copy_apply, Kernel.deterministic_apply]
 
-instance deterministic_Deterministic (X Y : SFinKer) (f : X.carrier → Y.carrier)
+instance Deterministic_deterministic (X Y : SFinKer) (f : X.carrier → Y.carrier)
     (hf : Measurable f) :
     Deterministic (X := X) (Y := Y) (⟨Kernel.deterministic f hf, inferInstance⟩ : X ⟶ Y) where
   hom_comul := by
     ext : 1; dsimp
     rw [Kernel.id_parallelComp_comp_parallelComp_id]
     exact (Kernel.deterministic_comp_copy hf).symm
 
-lemma id_map_Deterministic (X Y : SFinKer) (f : X.carrier → Y.carrier) (hf : Measurable f) :
+lemma Deterministic_id_map (X Y : SFinKer) (f : X.carrier → Y.carrier) (hf : Measurable f) :
     Deterministic (X := X) (Y := Y) (⟨Kernel.id.map f, inferInstance⟩ : X ⟶ Y) where
   hom_comul := by cat_disch
 
 variable {X Y Z : SFinKer}
 
 instance : Deterministic (α_ X Y Z).hom :=
-  deterministic_Deterministic ((X ⊗ Y) ⊗ Z)
+  Deterministic_deterministic ((X ⊗ Y) ⊗ Z)
       (X ⊗ Y ⊗ Z) (MeasurableEquiv.prodAssoc) (MeasurableEquiv.measurable _)
 
 instance : Deterministic (λ_ X ).hom :=
-  id_map_Deterministic (𝟙_ SFinKer ⊗ X) X Prod.snd (by fun_prop)
+  Deterministic_id_map (𝟙_ SFinKer ⊗ X) X Prod.snd (by fun_prop)
 
 instance : Deterministic (ρ_ X ).hom :=
-  id_map_Deterministic (X ⊗ 𝟙_ SFinKer) X Prod.fst (by fun_prop)
+  Deterministic_deterministic (X ⊗ 𝟙_ SFinKer) X Prod.fst (by fun_prop)
 
 instance : Deterministic (β_ X Y).hom :=
-  deterministic_Deterministic (X ⊗ Y) (Y ⊗ X) Prod.swap (by fun_prop)
+  Deterministic_deterministic (X ⊗ Y) (Y ⊗ X) Prod.swap (by fun_prop)
 
 instance : Deterministic (ε[X]) :=
-  deterministic_Deterministic X (𝟙_ SFinKer) (fun (x : X) ↦ PUnit.unit) (by fun_prop)
+  Deterministic_deterministic X (𝟙_ SFinKer) (fun (x : X) ↦ PUnit.unit) (by fun_prop)
 
 instance : Deterministic (Δ[X]) :=
-  deterministic_Deterministic X (X ⊗ X) (fun (x : X) ↦ (x, x)) (by fun_prop)
+  Deterministic_deterministic X (X ⊗ X) (fun (x : X) ↦ (x, x)) (by fun_prop)
 
 end