From 3d6127cd89b9909c86dad16db0aebad4d36d2464 Mon Sep 17 00:00:00 2001 From: YOSHIHIRO Imai Date: Fri, 2 Aug 2024 14:55:45 +0900 Subject: [PATCH] fix typo in measure.v --- theories/measure.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/measure.v b/theories/measure.v index f1e4c9a49..4bbe516c1 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -243,7 +243,7 @@ From HB Require Import structures. (* outer measure mu, i.e., sets A such that *) (* forall B, mu A = mu (A `&` B) + mu (A `&` ~` B) *) (* caratheodory_type mu := T, where mu : {outer_measure set T -> \bar R} *) -(* It is a canonical mesurableType copy of T. *) +(* It is a canonical measurableType copy of T. *) (* The restriction of the outer measure mu to the *) (* sigma algebra of Caratheodory measurable sets is a *) (* measure. *)