Skip to content

Commit

Permalink
fix typo in measure.v
Browse files Browse the repository at this point in the history
  • Loading branch information
yoshihiro503 authored and affeldt-aist committed Aug 2, 2024
1 parent f89df72 commit 3d6127c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion theories/measure.v
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down

0 comments on commit 3d6127c

Please sign in to comment.