From e13957b466bf93e32c669410b24d5ecb786143aa Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 6 Mar 2026 22:59:11 +0900 Subject: [PATCH] fix comment in convex.v --- probability/convex.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/probability/convex.v b/probability/convex.v index a35f79af..6170b2f4 100644 --- a/probability/convex.v +++ b/probability/convex.v @@ -26,9 +26,9 @@ From mathcomp.analysis Require Import (canonicals)convex. (* convType == the type of convex spaces, i.e., a choiceType with an *) (* operator x <| p |> y where p is a probability *) (* satisfying the following axioms: *) -(* conv1 == a <| 1%:pr |> b = a. *) +(* conv1 == a <| 1%:i01 |> b = a. *) (* convmm == a <| p |> a = a. *) -(* convC == a <| p |> b = b <| p.~%:pr |> a. *) +(* convC == a <| p |> b = b <| p.~%:i01 |> a. *) (* convA == a <| p |> (b <| q |> c) = *) (* (a <| [r_of p, q] |> b) <| [s_of p, q] |> c. *) (* <|>_d f == generalization of the conv operator . <| . |> . *)