From 730777b864cafcd4e26d97fd878334e59683ed01 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr> Date: Fri, 11 Mar 2022 19:51:09 +0100 Subject: [PATCH] Order (imports) + renaming (section). --- Lebesgue/measurable_R.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Lebesgue/measurable_R.v b/Lebesgue/measurable_R.v index 9370be2e..30d0afdf 100644 --- a/Lebesgue/measurable_R.v +++ b/Lebesgue/measurable_R.v @@ -17,9 +17,10 @@ COPYING file for more details. From Coq Require Import Qreals Reals Lra. From Coquelicot Require Import Hierarchy. -Require Import countable_sets topo_bases_R R_compl. +Require Import R_compl countable_sets topo_bases_R. Require Import Subset Subset_dec Subset_seq Subset_R. -Require Import Subset_system_base Subset_system measurable. +Require Import Subset_system_base Subset_system. +Require Import measurable. Open Scope R_scope. @@ -41,7 +42,7 @@ Inductive gen_R_Qoo : (R -> Prop) -> Prop := End gen_R_Def. -Section gen_R_eq. +Section measurable_R_Borel_eq. Lemma measurable_R_Borel_singleton : forall (x : R), measurable_Borel (singleton x). Proof. @@ -214,7 +215,7 @@ apply measurable_Borel_closed, closed_le. apply measurable_R_Borel_eq_oc. Qed. -End gen_R_eq. +End measurable_R_Borel_eq. Section measurable_R. -- GitLab