From 913a929ac6f190eb8159ecb51c863bd26715d84e Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 28 Mar 2024 10:09:38 +0900
Subject: [PATCH] typo

---
 probability/proba.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/probability/proba.v b/probability/proba.v
index ff1e0616..cd5804cb 100644
--- a/probability/proba.v
+++ b/probability/proba.v
@@ -1272,7 +1272,7 @@ Notation R := real_realType.
 
 Variables (A I : finType) (k : nat) (d : R.-fdist A) (E : I -> {set A}).
 
-Definition kwide_inde := forall (J : {set I}), (#|J| <= k)%nat ->
+Definition kwise_inde := forall (J : {set I}), (#|J| <= k)%nat ->
   Pr d (\bigcap_(i in J) E i) = \prod_(i in J) Pr d (E i).
 
 End k_wise_independence.
@@ -1282,7 +1282,7 @@ Notation R := real_realType.
 
 Variables (A I : finType) (d : R.-fdist A) (E : I -> {set A}).
 
-Definition pairwise_inde := @kwide_inde A I 2%nat d E.
+Definition pairwise_inde := @kwise_inde A I 2%nat d E.
 
 Lemma pairwise_indeE :
   pairwise_inde <-> (forall i j, i != j -> inde_events d (E i) (E j)).
@@ -1311,7 +1311,7 @@ Notation R := real_realType.
 
 Variables (A I : finType) (d : R.-fdist A) (E : I -> {set A}).
 
-Definition mutual_inde := (forall k, @kwide_inde A I k.+1 d E).
+Definition mutual_inde := (forall k, @kwise_inde A I k.+1 d E).
 
 Lemma mutual_indeE :
   mutual_inde <-> (forall J : {set I}, J \subset I ->
@@ -1324,7 +1324,7 @@ rewrite /mutual_inde; split => [H J JI|H k J JI].
 by rewrite H //; apply/subsetP => i ij; rewrite inE.
 Qed.
 
-Lemma mutual_indeE' : #|I| != O -> mutual_inde <-> kwide_inde #|I| d E.
+Lemma mutual_indeE' : #|I| != O -> mutual_inde <-> kwise_inde #|I| d E.
 Proof.
 move=> I0.
 rewrite /mutual_inde; split => [H J JI|].