From 2129372e2acb6d58aa76a781954df8991b44bc21 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr> Date: Thu, 31 Mar 2022 00:46:03 +0200 Subject: [PATCH] Use new Subset_system_def. --- Lebesgue/Subset_R.v | 2 +- Lebesgue/Subset_Rbar.v | 2 +- Lebesgue/Subset_system.v | 6 +++--- Lebesgue/Subset_system_gen.v | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Lebesgue/Subset_R.v b/Lebesgue/Subset_R.v index ead5822e..5dd48418 100644 --- a/Lebesgue/Subset_R.v +++ b/Lebesgue/Subset_R.v @@ -19,7 +19,7 @@ From Coquelicot Require Import Coquelicot. Require Import R_compl Rbar_compl countable_sets topo_bases_R. Require Import Subset Subset_dec Subset_seq. -Require Import Subset_system_base. +Require Import Subset_system_def Subset_system_base. Open Scope R_scope. diff --git a/Lebesgue/Subset_Rbar.v b/Lebesgue/Subset_Rbar.v index 52543038..48e863e1 100644 --- a/Lebesgue/Subset_Rbar.v +++ b/Lebesgue/Subset_Rbar.v @@ -20,7 +20,7 @@ From Coquelicot Require Import Coquelicot. Require Import nat_compl countable_sets. Require Import R_compl Rbar_compl UniformSpace_compl topo_bases_R. Require Import Subset Subset_dec Subset_seq. -Require Import Subset_system_base Subset_R. +Require Import Subset_system_def Subset_system_base Subset_R. Open Scope R_scope. diff --git a/Lebesgue/Subset_system.v b/Lebesgue/Subset_system.v index fbf01430..fcd8c5cf 100644 --- a/Lebesgue/Subset_system.v +++ b/Lebesgue/Subset_system.v @@ -21,8 +21,8 @@ COPYING file for more details. From Coq Require Import ClassicalChoice. Require Import nat_compl. -Require Import Subset Subset_dec Subset_finite Subset_seq. -Require Import Subset_system_base Subset_system_gen. +Require Import Subset Subset_dec Subset_finite Subset_seq Function. +Require Import Subset_system_def Subset_system_base Subset_system_gen. Section Subset_systems_Def1. @@ -2440,7 +2440,7 @@ right; rewrite HA2; apply compl_empty. left; rewrite HA2; apply compl_full. case (excluded_middle_informative (exists n, A n = fullset)); intros H. right; now apply union_seq_full. -left; apply empty_union_seq; intros n; destruct (HA2 n) as [HA2' | HA2']; try easy. +left; apply union_seq_empty; intros n; destruct (HA2 n) as [HA2' | HA2']; try easy. contradict H; now exists n. Qed. diff --git a/Lebesgue/Subset_system_gen.v b/Lebesgue/Subset_system_gen.v index ffafedea..b41d5ec0 100644 --- a/Lebesgue/Subset_system_gen.v +++ b/Lebesgue/Subset_system_gen.v @@ -14,7 +14,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. *) -Require Import Subset Subset_system_base. +Require Import Subset Subset_system_def Subset_system_base. Section Subset_system_Gen_Def0. -- GitLab