From 3fe5596c58dcae20f0667933a3571f745599a898 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Mon, 16 Feb 2026 18:38:16 +0900 Subject: [PATCH 1/2] add `itv_closureE`, `itv_interiorE`, and helper lemmas --- CHANGELOG_UNRELEASED.md | 21 ++ classical/classical_sets.v | 61 +++- classical/set_interval.v | 170 ++++++++++- classical/unstable.v | 205 ++++++++++++++ theories/topology_theory/num_topology.v | 267 +++++++++++++++++- theories/topology_theory/topology_structure.v | 43 +++ 6 files changed, 753 insertions(+), 14 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 318217cd5..a35f9b3ba 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -3,6 +3,24 @@ ## [Unreleased] ### Added +- in classical_sets.v + + lemma `powerset0`, `powerset1`, `powerset2`, `powersetS`, + `setorder_itv_setUl_image`, `setorder_itv_setUr_image`, + `setorder_itv_setDl_image` + +- in set_interval.v + + lemmas `itv_open_endsPn`, `itv_closed_endsPn`, `itv_open_ends_boundlr`, + `setUitv2`, `setDitv2`, `setDitvoo`, `setDitvoy`, `setDitvNyo`, + `setDccitv`, `setDcitvy`, `setDcitvNy` + +- in topology_structure.v + + lemmas `closureEbigcap_itvcy`,`interiorEbigcup_itvNyc`, + `closureEbigcap_itvcc`,`interiorEbigcup_itvcc` + +- in num_topology.v + + lemmas `open_itv_open_ends`, `closed_itv_closed_ends`, + `itv_closureE`, `itv_interiorE` + - in order_topology.v + lemma `itv_closed_ends_closed` - in classical_sets.v @@ -22,6 +40,9 @@ + lemmas `pmf_gt0_countable`, `pmf_measurable` ### Changed +- in set_interval.v + + `setDitv1l`, `setDitv1r` (generalized) + - in set_interval.v + `itv_is_closed_unbounded` (fix the definition) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 99c60f144..c125896ed 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -218,6 +218,8 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Declare Scope classical_set_scope. +Declare Scope relation_scope. +Delimit Scope relation_scope with relation. Reserved Notation "[ 'set' x : T | P ]" (only parsing). Reserved Notation "[ 'set' x | P ]" (format "[ 'set' x | P ]"). @@ -3339,14 +3341,12 @@ Proof. by apply/seteqP; split; move=> x/=; rewrite /ysection/= inE. Qed. End section. -Declare Scope relation_scope. -Delimit Scope relation_scope with relation. - Notation "B \; A" := ([set xy | exists2 z, A (xy.1, z) & B (z, xy.2)]) : relation_scope. Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : relation_scope. +Section relation. Local Open Scope relation_scope. Lemma set_compose_subset {X Y : Type} (A C : set (X * Y)) (B D : set (Y * X)) : @@ -3370,4 +3370,57 @@ Definition diagonal {T : Type} := [set x : T * T | x.1 = x.2]. Lemma diagonalP {T : Type} (x y : T) : diagonal (x, y) <-> x = y. Proof. by []. Qed. -Local Close Scope relation_scope. +End relation. + +Lemma powerset0 {T : Type} : + [set X | X `<=` set0] = [set set0] :> set (set T). +Proof. by apply/funext => X /=; rewrite subset0. Qed. + +Lemma powerset1 {T : Type} (a : T) : + [set X | X `<=` [set a]] = [set set0; [set a]]. +Proof. by apply/seteqP; split => X/=; [move/subset_set1|case=> ->]. Qed. + +Lemma powerset2 {T : Type} (a b : T) : + [set X | X `<=` [set a; b]] = [set set0; [set a]; [set b]; [set a; b]]. +Proof. +apply/seteqP; split => X/=; first by move/subset_set2; rewrite or4E !orA. +by move=> [[[]|]|] ->. +Qed. + +Lemma powersetS {T : Type} (A B : set T) : + (A `<=` B) = ([set X | X `<=` A] `<=` [set X | X `<=` B]). +Proof. +apply: propext; split; first by move=> AB X/= /subset_trans; apply. +by move=> + a Aa => /(_ [set a])/= /(_ _ a); apply => // ? ->. +Qed. + +Lemma setorder_itv_setUl_image {T : Type} (A B : set T) : + A `<=` B -> + `[A, B]%classic = (setU A) @` [set X | X `<=` B `\` A]. +Proof. +move=> AB; apply/seteqP; split => Y/=. + rewrite in_itv/= => /andP[]; rewrite !subsetEset => AY YB. + by exists (Y `\` A); [exact: setSD | rewrite setDUK]. +case=> X XBA <-; rewrite in_itv/= Order.JoinTheory.leUl/=. +by rewrite -(setDUK AB) Order.JoinTheory.leU2// subsetEset. +Qed. + +Lemma setorder_itv_setUr_image {T : Type} (A B : set T) : + A `<=` B -> + `[A, B]%classic = (setU^~ A) @` [set X | X `<=` B `\` A]. +Proof. +by (under eq_imagel do rewrite setUC); exact: setorder_itv_setUl_image. +Qed. + +Lemma setorder_itv_setDl_image {T : Type} (A B : set T) : + A `<=` B -> + `[A, B]%classic = (setD B) @` [set X | X `<=` B `\` A]. +Proof. +move=> AB; apply/seteqP; split => Y/=. + rewrite in_itv/= => /andP[]; rewrite !subsetEset => AY YB. + by exists (B `\` Y); [exact: setDS | rewrite setDD setIidr]. +case=> X XBA <-; rewrite in_itv/= Order.MeetTheory.leIl andbT. +rewrite (@Order.POrderTheory.le_trans _ _ (B `\` (B `\` A)))//; last first. + by rewrite subsetEset; exact: setDS. +by rewrite setDD setIidr. +Qed. diff --git a/classical/set_interval.v b/classical/set_interval.v index 7008aadd0..1645fb144 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -182,31 +182,55 @@ Definition set_itvE := (set_itv1, set_itvoo0, set_itvoc0, set_itvco0, set_itvoo, Lemma set_itvxx a : [set` Interval a a] = set0. Proof. by move: a => [[|] a |[|]]; rewrite !set_itvE. Qed. -Lemma setUitv1 a x : (a <= BLeft x)%O -> - [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)]. +Let setUitv1_gen a x b : (a <= BLeft x)%O -> + [set` Interval a (BSide b x)] `|` [set x] = [set` Interval a (BRight x)]. +Proof. +move=> ax; case: b; last first. + by apply: setUidl => ? /= ->; rewrite itv_boundlr ax lexx. +apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE. +by rewrite (rwP eqP) (rwP orP) orbC. +Qed. + +Let setU1itv_gen a x b : (BRight x <= a)%O -> + x |` [set` Interval (BSide b x) a] = [set` Interval (BLeft x) a]. Proof. -move=> ax; apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE. +move=> ax; case: b. + by apply: setUidr => ? /= ->; rewrite itv_boundlr ax lexx. +apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE. by rewrite (rwP eqP) (rwP orP) orbC. Qed. +Lemma setUitv1 a x : (a <= BLeft x)%O -> + [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)]. +Proof. exact: setUitv1_gen. Qed. + Lemma setU1itv a x : (BRight x <= a)%O -> x |` [set` Interval (BRight x) a] = [set` Interval (BLeft x) a]. +Proof. exact: setU1itv_gen. Qed. + +Lemma setUitv2 x y b1 b2 : + (x <= y)%O -> + [set` Interval (BSide b1 x) (BSide b2 y)] `|` [set x; y] = `[x, y]%classic. Proof. -move=> ax; apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE. -by rewrite (rwP eqP) (rwP orP) orbC. +rewrite le_eqVlt => /orP [/eqP->|xy]. + by case: b1; case: b2; rewrite !set_itvE !setUid // set0U. +rewrite setUCA setUitv1_gen; last by case: b1; rewrite bnd_simp// ltW. +by rewrite setU1itv_gen// bnd_simp ltW. Qed. -Lemma setDitv1r a x : - [set` Interval a (BRight x)] `\ x = [set` Interval a (BLeft x)]. +Lemma setDitv1r a x b : + [set` Interval a (BSide b x)] `\ x = [set` Interval a (BLeft x)]. Proof. +case: b; first by apply: not_setD1; rewrite /= in_itv/= ltxx andbF. apply/seteqP; split => [z|z] /=; rewrite !in_itv/=. by move=> [/andP[-> /= zx] /eqP xz]; rewrite lt_neqAle xz. by rewrite lt_neqAle => /andP[-> /andP[/eqP ? ->]]. Qed. -Lemma setDitv1l a x : - [set` Interval (BLeft x) a] `\ x = [set` Interval (BRight x) a]. +Lemma setDitv1l a x b : + [set` Interval (BSide b x) a] `\ x = [set` Interval (BRight x) a]. Proof. +case: b; last by apply: not_setD1; rewrite /= in_itv/= ltxx. apply/seteqP; split => [z|z] /=; rewrite !in_itv/=. move=> [/andP[xz ->]]; rewrite andbT => /eqP. by rewrite lt_neqAle eq_sym => ->. @@ -214,6 +238,10 @@ move=> /andP[]; rewrite lt_neqAle => /andP[xz zx ->]. by rewrite andbT; split => //; exact/nesym/eqP. Qed. +Lemma setDitv2 x y b1 b2 : + [set` Interval (BSide b1 x) (BSide b2 y)] `\` [set x; y] = `]x, y[%classic. +Proof. by rewrite -setDDl setDitv1l setDitv1r. Qed. + End set_itv_porderType. Arguments neitv {disp T} _. #[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `set_itvNyy`")] @@ -314,6 +342,95 @@ move=> cab; apply/seteqP; split => [x /= [xab /eqP]|x[|]]/=. by apply/eqP; rewrite gt_eqF. Qed. +Lemma setDitvoo (x y : T) (b1 b2 : bool) : + [set` Interval (BSide b1 x) (BSide b2 y)] != set0 -> + [set` Interval (BSide b1 x) (BSide b2 y)] `\` `]x, y[ = + (if b1 then [set x] else set0) `|` (if b2 then set0 else [set y]). +Proof. +case/set0P => u /= /itv_boundlr_lt xy. +apply/seteqP; split => z/=; rewrite !in_itv/=; last first. + move: b1 b2 xy. + case=> -[]; rewrite !bnd_simp/= => + []// -> => ->; rewrite ?lexx ?ltxx//. + by rewrite andbF. +case=> /[swap] /negP; rewrite negb_and. +move: b1 b2 {xy}. +case=> -[]/= + /andP[]; rewrite ?ltNge !negbK => /orP[]; try move=> -> //. +- by case; move=> ? ? ?; left; apply/le_anti/andP; split. +- by case; move=> ? ? ?; left; apply/le_anti/andP; split. +- by case; move=> ? ? ?; right; apply/le_anti/andP; split. +- by case; move=> ? ? ?; right; apply/le_anti/andP; split. +Qed. + +Lemma setDccitv (x y : T) (b1 b2 : bool) : + `[x, y]%classic != set0 -> + `[x, y] `\` [set` Interval (BSide b1 x) (BSide b2 y)] = + (if b1 then set0 else [set x]) `|` (if b2 then [set y] else set0). +Proof. +case/set0P => u /= /itv_boundlr_lt xy. +apply/seteqP; split => z/=; rewrite !in_itv/=; last first. + move: b1 b2 xy. + case=> -[]; rewrite !bnd_simp/= => + []// -> => ->; rewrite ?lexx ?ltxx//. + by rewrite andbF. +case=> /[swap] /negP; rewrite negb_and. +move: b1 b2 {xy}. +case=> -[]/= /orP[] + /andP[]; rewrite -?leNgt; try move=> /negPf -> //. +- by move=> ? ? ?; right; apply/le_anti/andP; split. +- by move=> ? ? ?; left; apply/le_anti/andP; split. +- by move=> ? ? ?; right; apply/le_anti/andP; split. +- by move=> ? ? ?; left; apply/le_anti/andP; split. +Qed. + +Lemma setDitvoy a (x : T) (b : bool) : + [set` Interval (BSide b x) a] != set0 -> + [set` Interval (BSide b x) a] `\` `]x, +oo[ = + (if b then [set x] else set0). +Proof. +case/set0P => u xau. +apply/seteqP; split => z/=; rewrite !in_itv/=; last first. + move: xau; case: b; rewrite //= => /[swap] <-. + by case: a => [[]?|[]] /itv_boundlr_lt; rewrite /= !bnd_simp. +clear xau; case: b; rewrite /= andbT; last by case=> /andP[] ->. +by case=> /andP[] ? _ /negP; rewrite -leNgt => ?; apply/le_anti/andP; split. +Qed. + +Lemma setDitvNyo a (x : T) (b : bool) : + [set` Interval a (BSide b x)] != set0 -> + [set` Interval a (BSide b x)] `\` `]-oo, x[ = + (if b then set0 else [set x]). +Proof. +case/set0P => u xau. +apply/seteqP; split => z/=; rewrite !in_itv/=; last first. + move: xau; case: b => //= /[swap] <-. + by case: a => [[]?|[]] /itv_boundlr_lt; rewrite /= !bnd_simp// andbT. +clear xau; case: b => /=; first by case=> /andP[] _ ->. +by case=> /andP[] _ ? /negP; rewrite -leNgt => ?; apply/le_anti/andP; split. +Qed. + +Lemma setDcitvy a (x : T) (b : bool) : + [set` Interval (BLeft x) a] != set0 -> + [set` Interval (BLeft x) a] `\` [set` Interval (BSide b x) +oo%O] = + (if b then set0 else [set x]). +Proof. +case/set0P => u xau. +apply/seteqP; split => z/=; rewrite !in_itv/=; last first. + move: xau; case: b => //= /[swap] <-. + by case: a => [[]?|[]] /itv_boundlr_lt; rewrite /= !bnd_simp. +clear xau; case: b; rewrite /= andbT; first by case=> /andP[] ->. +by case=> /andP[] ? _ /negP; rewrite -leNgt => ?; apply/le_anti/andP; split. +Qed. + +Lemma setDcitvNy a (x : T) (b : bool) : + [set` Interval a (BRight x)] != set0 -> + [set` Interval a (BRight x)] `\` [set` Interval -oo%O (BSide b x)] = + (if b then [set x] else set0). +case/set0P => u xau. +apply/seteqP; split => z/=; rewrite !in_itv/=; last first. + move: xau; case: b; rewrite //= => /[swap] <-. + by case: a => [[]?|[]] /itv_boundlr_lt; rewrite /= !bnd_simp// andbT. +clear xau; case: b => /=; last by case=> /andP[] _ ->. +by case=> /andP[] _ ? /negP; rewrite -leNgt => ?; apply/le_anti/andP; split. +Qed. + End set_itv_orderType. Lemma set_itv_ge disp [T : porderType disp] [b1 b2 : itv_bound T] : @@ -893,3 +1010,38 @@ Lemma itv_setI {d} {T : orderType d} (i j : interval T) : Proof. by rewrite eqEsubset; split => z; rewrite /in_mem/= /pred_of_itv/= lexI=> /andP. Qed. + +Lemma itv_open_endsPn {d} {T : porderType d} (l r : itv_bound T) : + (l < r)%O -> + reflect + (exists x : T , l = BLeft x \/ r = BRight x) + (~~ itv_open_ends (Interval l r)). +Proof. +move=> lr. +apply: (iffP idP); last first. + by clear lr; case=> x [] -> //; case: l => [[] ?|[]]. +move: lr; case: l => [[] L|[]] //; case: r => [[] R|[]]//= ? ?. +all: try (by exists L; left); by exists R; right. +Qed. + +Lemma itv_closed_endsPn {d} {T : porderType d} (l r : itv_bound T) : + (l < r)%O -> + reflect + (exists x : T , l = BRight x \/ r = BLeft x) + (~~ itv_closed_ends (Interval l r)). +Proof. +move=> lr. +apply: (iffP idP); last first. + by clear lr; case=> x [] -> //; case: l => [[] ?|[]]. +move: lr; case: l => [[] L|[]] //; case: r => [[] R|[]]//= ? ?. +all: try (by exists L; left); by exists R; right. +Qed. + +Lemma itv_open_ends_boundlr {d} {T : porderType d} (bl br : itv_bound T) (x : T) : + itv_open_ends (Interval bl br) -> + (x \in Interval bl br) = (bl < BLeft x)%O && (BRight x < br)%O. +Proof. +rewrite itv_boundlr !le_eqVlt. +have [->|_] := eqVneq bl (BLeft x); first by move/itv_open_ends_lside. +by have [->|_] := eqVneq br (BRight x); first by move/itv_open_ends_rside. +Qed. diff --git a/classical/unstable.v b/classical/unstable.v index da4e0b808..ed7109560 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -553,3 +553,208 @@ End ProperNotations. Lemma sqrtK {K : rcfType} : {in Num.nneg, cancel (@Num.sqrt K) (fun x => x ^+ 2)}. Proof. by move=> r r0; rewrite sqr_sqrtr. Qed. + +Section interval. +Local Open Scope order_scope. +Variable (disp : Order.disp_t) (T : porderType disp). +Implicit Types (x y z : T) (b bl br : itv_bound T) (i : interval T). + +Lemma itv_boundlr_lt bl br x : x \in Interval bl br -> bl < br. +Proof. +rewrite itv_boundlr => /andP[] lx. +by apply/lt_le_trans/(le_lt_trans lx); rewrite bnd_simp. +Qed. + +End interval. + +Module EndlessDenseOrderTheory. + +Section theory. +Local Open Scope order_scope. +(*Local Open Scope classical_set_scope.*) + +Definition is_endless_porderType {d} (T : porderType d) := + forall x : T, (exists y, y < x) /\ (exists y, x < y). + +Definition is_dense_porderType {d} (T : porderType d) := + forall x y : T, x < y -> exists z, x < z < y. + +Let fin_itv_bound_half_dense {d} {T : porderType d} bl br (L R : T) : + is_dense_porderType T -> + BSide bl L < BSide br R -> + exists y, BSide bl L <= BLeft y < BSide br R. +Proof. +move=> T_dense. +case: bl; case: br; rewrite !bnd_simp. +- by exists L; rewrite !bnd_simp. +- by exists R; rewrite !bnd_simp andbT. +- by case/T_dense => y ?; exists y; rewrite !bnd_simp. +- by exists R; rewrite !bnd_simp andbT. +Qed. + +Let linfty_itv_bound_half_dense {d} {T : porderType d} (x : T) bl (j : itv_bound T) : + is_endless_porderType T -> + BInfty _ bl < j -> + exists y, BInfty _ bl <= BLeft y < j. +Proof. +move=> T_endless. +case: bl; case: j => [[] J | []//]; rewrite !bnd_simp//. +- by have [[y ?] _] := T_endless J; exists y; rewrite !bnd_simp. +- by exists J; rewrite !bnd_simp. +- by exists x; rewrite !bnd_simp. +Qed. + +Let rinfty_itv_bound_half_dense {d} {T : porderType d} (x : T) br (i : itv_bound T) : + is_endless_porderType T -> + i < BInfty _ br -> + exists y, i <= BLeft y < BInfty _ br. +Proof. +move=> T_endless. +case: br; case: i => [[] I | []//]; rewrite !bnd_simp//. +- by exists I; rewrite !bnd_simp. +- by have [_ [y ?]] := T_endless I; exists y; rewrite !bnd_simp andbT. +- by exists x; rewrite !bnd_simp. +Qed. + +Lemma itv_bound_half_dense {d} {T : porderType d} (x : T) (i j : itv_bound T) : + is_endless_porderType T -> + is_dense_porderType T -> + i < j -> exists y, i <= BLeft y < j. +Proof. +move=> T_endless T_dense. +case: i => [? ? | ?]; case j => [? ? | ?]. +- exact: fin_itv_bound_half_dense. +- exact: rinfty_itv_bound_half_dense. +- exact: linfty_itv_bound_half_dense. +- exact: linfty_itv_bound_half_dense. +Qed. + +Let subitvP_half1 {d} {T : orderType d} (i j : interval T) x : + is_endless_porderType T -> + is_dense_porderType T -> + x \in i -> {subset i <= j} -> j.1 <= i.1. +Proof. +case: i => il ir; case: j => jl jr /=. +move=> T_endless T_dense xi isubj. +have := xi; rewrite itv_boundlr => /andP[] _ xir. +have := isubj _ xi; rewrite itv_boundlr => /andP[] jlx _. +rewrite leNgt; apply/negP => /itv_bound_half_dense [] // y /andP[ily yjl]. +suff/isubj : y \in Interval il ir by rewrite itv_boundlr leNgt yjl. +rewrite itv_boundlr ily/= (le_trans _ xir)// ltW//. +by have:= lt_le_trans yjl jlx; rewrite !bnd_simp. +Qed. + +Definition dual_itv_bound {d} {T : porderType d} (ib : itv_bound T) : + itv_bound T^d := + match ib with + | BInfty b => BInfty _ (~~ b) + | BSide b x => BSide (~~ b) x + end. + +Definition dual_itv {d} {T : porderType d} (i : interval T) : interval T^d := + @Interval T^d (dual_itv_bound i.2) (dual_itv_bound i.1). + +Lemma dual_itvE {d} {T : porderType d} (i : interval T) : + dual_itv i =i i. +Proof. +case: i => l r; move=> p; rewrite /dual_itv /dual_itv_bound. +case: l => [[] x | []]; case: r => [[] y | []]//=. +all: rewrite /= !in_itv/= !(@in_itv d T)/= ?ltEdual ?leEdual. +all: by rewrite ?andbT// ?andbF// andbC. +Qed. + +Lemma dual_itv_sub_memP {d} {T : porderType d} (i j : interval T) : + {subset i <= j} <-> {subset dual_itv i <= dual_itv j}. +Proof. by split => + x => /(_ x); rewrite !dual_itvE. Qed. + +Lemma dual_is_dense {d} {T : porderType d} : + is_dense_porderType T -> is_dense_porderType T^d. +Proof. +move=> + x y xy /= => /(_ y x xy) [] z yzx. +by exists z; rewrite !ltEdual andbC. +Qed. + +Lemma dual_is_endless {d} {T : porderType d} : + is_endless_porderType T -> is_endless_porderType T^d. +Proof. +move=> + x => /(_ x) [[y yx] [z xz]]; split. + by exists z; rewrite ltEdual. +by exists y; rewrite ltEdual. +Qed. + +Lemma dual_itv_boundK {d} {T : porderType d} (ib : itv_bound T) : + dual_itv_bound (dual_itv_bound ib) = ib. +Proof. by case: ib => [[]?|[]]. Qed. + +Lemma dual_itv_bound_lt {d} {T : porderType d} (l r : itv_bound T) : + (dual_itv_bound l < dual_itv_bound r) = (r < l). +Proof. by case: l => [[]?|[]]; case: r => [[]?|[]]. Qed. + +Lemma dual_itv_bound_le {d} {T : porderType d} (l r : itv_bound T) : + (dual_itv_bound l <= dual_itv_bound r) = (r <= l). +Proof. by case: l => [[]?|[]]; case: r => [[]?|[]]. Qed. + +Let subitvP_half2 {d} {T : orderType d} (i j : interval T) x : + is_endless_porderType T -> + is_dense_porderType T -> + x \in i -> {subset i <= j} -> i.2 <= j.2. +Proof. +case: i => il ir; case: j => jl jr. +move=> /dual_is_endless T_endless /dual_is_dense T_dense. +rewrite -dual_itvE => xi /dual_itv_sub_memP isubj. +have := @subitvP_half1 _ T^d. +move/(_ (dual_itv (Interval il ir)) (dual_itv (Interval jl jr)) x). +move/(_ T_endless T_dense xi isubj). +by rewrite dual_itv_bound_le. +Qed. + +Lemma subitvP {d} {T : orderType d} (i j : interval T) x : + is_endless_porderType T -> + is_dense_porderType T -> + x \in i -> + i <= j <-> {subset i <= j}. +Proof. +case: i => ? ?; case: j => ? ?. +move=> *; split; first exact: subitvP. +move=> isubj; apply/andP; split. + move/(@subitvP_half1 _ _ _ _ x): isubj; exact. +move/(@subitvP_half2 _ _ _ _ x): isubj; exact. +Qed. + +End theory. + +Section num. +Local Open Scope ring_scope. + +Lemma numDomain_is_endless (R : numDomainType) : is_endless_porderType R. +Proof. +move=> x; split. + by exists (x - 1); rewrite gtrBl. +by exists (x + 1); rewrite ltrDl. +Qed. + +Lemma numField_is_dense (R : numFieldType) : is_dense_porderType R. +Proof. +move=> x y xy; exists (2^-1 * (x + y)). +rewrite -(@ltr_pM2l _ 2)// -[X in _ && X](@ltr_pM2l _ 2)//. +rewrite mulrA divff ?lt0r_neq0// mul1r !mulr_natl !mulr2n. +by rewrite ltrD2l ltrD2r xy. +Qed. + +End num. + +End EndlessDenseOrderTheory. + +Section interval_realFieldType. +Variable R : realFieldType. +Implicit Types x : R. +Local Open Scope order_scope. + +Let R_is_endless := @EndlessDenseOrderTheory.numDomain_is_endless R. +Let R_is_dense := @EndlessDenseOrderTheory.numField_is_dense R. + +Lemma real_subitvP (i j : interval R) x : + x \in i -> i <= j <-> {subset i <= j}. +Proof. exact: EndlessDenseOrderTheory.subitvP. Qed. + +End interval_realFieldType. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index df7c804f2..3f70fe910 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -1,7 +1,10 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_classical. -From mathcomp Require Import interval_inference reals topology_structure. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import interval_inference reals real_interval. +From mathcomp Require Import topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure. From mathcomp Require Import order_topology matrix_topology. @@ -488,3 +491,265 @@ move=> u A /nbhs_ballP[e /= e0 eA]. apply/nbhs_ballP; exists e => //= v [_ uv]; apply: eA; split => // i j. by apply: (le_lt_trans _ (uv i (lshift n2 j))); rewrite !mxE. Qed. + +(* An internal theory prepared for the next section (realField_topology). *) +(* This module itself is all about order_topology and says nothing specific *) +(* to num_topology. *) +Module EndlessDenseOrderTopologyTheory. +Import unstable.EndlessDenseOrderTheory. + +Section theory. + +Local Open Scope order_scope. +Local Open Scope classical_set_scope. +Context {d} {T : orderTopologicalType d}. +Implicit Types x y : T. + +Lemma open_itv_open_ends (i : interval T) : + is_endless_porderType T -> is_dense_porderType T -> [set` i] != set0 -> + open [set` i] -> itv_open_ends i. +Proof. +move=> T_endless T_dense. +case: i => l r /set0P[?/=] /itv_boundlr_lt lr. +rewrite openE /interior/=. +(under [X in X -> _]eq_forall do rewrite itv_nbhsE/=) => i_open. +apply/negbNE/negP; case/(itv_open_endsPn lr) => x lrx. +have: x \in Interval l r. + move: lr; case: lrx => ->; rewrite itv_boundlr lexx ?leBRight_ltBLeft//. + by rewrite ltBRight_leBLeft => ->. +case/i_open => -[l' r'] [] + xj; rewrite -subset_itvP => /[swap]. +have := xj; rewrite itv_boundlr => /andP[l'x xr']. +rewrite -subitvP//; last exact: xj. +rewrite subitvE => /andP[] ll' r'r. +apply/negP/itv_open_endsPn; [exact: (itv_boundlr_lt xj) | exists x]. +move: l'x xr' ll' r'r. +by case: lrx => <-; [left|right]; apply/le_anti/andP; split. +Qed. + +Lemma closed_itv_closed_ends (i : interval T) : + is_endless_porderType T -> is_dense_porderType T -> [set` i] != set0 -> + closed [set` i] -> itv_closed_ends i. +Proof. +move=> T_endless T_dense. +case: i => l r /set0P[?/=] /itv_boundlr_lt lr. +rewrite closedE/= /prop_near1/=. +(under [X in X -> _]eq_forall do rewrite itv_nbhsE/=) => i_closed. +apply/negbNE/negP; case/(itv_closed_endsPn lr) => x lrx. +have: ~ (x \in Interval l r). + by case: lrx => ->; rewrite itv_boundlr !bnd_simp// andbF. +apply; apply: i_closed => -[[l' r'][]] /itv_open_ends_boundlr -> /andP[] l'x xr'. +move: lr; case: lrx => -> => [xr|lx]. + have : BRight x < Order.min r r' by rewrite lt_min xr xr'. + case/itv_bound_half_dense => // y /andP[] xy yr /(_ y); apply. + rewrite /= itv_boundlr. + have := yr; rewrite lt_min -!leBRight_ltBLeft => /andP[] _ ->. + by rewrite andbT (le_trans _ xy)// ltW// ltBRight_leBLeft ltW. + rewrite itv_boundlr xy/= leBRight_ltBLeft. + by have := yr; rewrite lt_min => /andP[]. +have : Order.max l l' < BLeft x by rewrite gt_max lx l'x. +case/itv_bound_half_dense => // y /andP[] ly yx /(_ y); apply. + rewrite /= itv_boundlr. + have := ly; rewrite ge_max => /andP[] _ -> /=. + by rewrite leBRight_ltBLeft (lt_trans yx)// -leBRight_ltBLeft ltW. +rewrite itv_boundlr leBRight_ltBLeft yx andbT. +by have := ly; rewrite ge_max => /andP[]. +Qed. + +Let itvoo_closureE (x y : T) : + is_endless_porderType T -> is_dense_porderType T -> `]x, y[ != set0 -> + closure `]x, y[ = `[x, y]. +Proof. +move=> T_endless T_dense /set0P[] u /itv_boundlr_lt /[!bnd_simp] xy. +have ineq0 bb1 bb2 : [set` Interval (BSide bb1 x) (BSide bb2 y)] != set0. + have[z /andP[xz zy]]:= T_dense x y xy. + apply/set0P; exists z; rewrite /= in_itv/=. + by case: bb1; case: bb2; apply/andP; split; rewrite /= ?ltW. +have subcc : `]x, y[ `<=` `[x, y] by apply: subset_itv; rewrite !bnd_simp. +apply/seteqP; split. + by rewrite (closure_id `[x, y]).1; [exact: closure_subset|exact: itv_closed]. +rewrite (closureEbigcap_itvcc `[x, y])//; last exact: itv_closed. +rewrite setorder_itv_setDl_image// setDitvoo//. +rewrite powerset2 !image_setU !image_set1 setD0 setDitv1l setDitv1r setDitv2. +rewrite setIC !setIUl => /= z ? i -[[[]|]|] []->// ci. +all: exfalso; move/closed_itv_closed_ends: ci. +all: cbn; rewrite falseE; apply => //. +all: exact: ineq0. +Qed. + +Lemma fin_itv_closureE (x y : T) b1 b2 : + is_endless_porderType T -> is_dense_porderType T -> + [set` Interval (BSide b1 x) (BSide b2 y)] != set0 -> + closure [set` Interval (BSide b1 x) (BSide b2 y)] = `[x, y]. +Proof. +move=> T_endless T_dense /set0P[] u /= /itv_boundlr_lt bxy. +have : x <= y by move: bxy; case: b1; case: b2; rewrite bnd_simp// => /ltW. +rewrite le_eqVlt => /orP[/eqP xy| xy]. + move: b1 b2 bxy; rewrite xy => -[][]; rewrite !bnd_simp// => _. + by rewrite -((closure_id `[y,y]).1)//; exact: itv_closed. +apply/seteqP; split. + rewrite (closure_id `[x, y]).1; last exact: itv_closed. + by apply/closure_subset/subset_itv; rewrite !bnd_simp. +rewrite -itvoo_closureE//. + by apply/closure_subset/subset_itv; rewrite !bnd_simp. +have[z /andP[xz zy]]:= T_dense x y xy. +by apply/set0P; exists z; rewrite /= in_itv/= xz zy. +Qed. + +Let itvoy_closureE (x : T) : + is_endless_porderType T -> is_dense_porderType T -> + closure `]x, +oo[ = `[x, +oo[. +Proof. +move=> T_endless T_dense. +have subcy : `]x, +oo[ `<=` `[x, +oo[. + by apply: subset_itv => //; rewrite !bnd_simp. +apply/seteqP; split. + rewrite (closure_id `[x, +oo[).1; first exact: closure_subset. + exact: rray_closed. +rewrite (closureEbigcap_itvcc `[x, +oo[)//; last exact: rray_closed. +rewrite setorder_itv_setDl_image// setDcitvy; last first. + by apply/set0P; exists x; rewrite /= in_itv/= lexx. +rewrite powerset1 image_setU !image_set1 setD0 setDitv1l setIC setIUl. +move=> /= z/= zx /= i [] [] -> // ci; exfalso. +move/closed_itv_closed_ends: ci; cbn; rewrite falseE; apply => //. +have[_ [y xy]]:= T_endless x. +by apply/set0P; exists y; rewrite /= in_itv/= xy. +Qed. + +Lemma rinfty_itv_closureE (x : T) b : + is_endless_porderType T -> is_dense_porderType T -> + closure [set` Interval (BSide b x) +oo] = `[x, +oo[. +Proof. +move=> T_endless T_dense. +have subcy: [set` Interval (BSide b x) +oo] `<=` `[x, +oo[. + by apply: subset_itv => //; rewrite !bnd_simp. +apply/seteqP; split. + rewrite (closure_id `[x, +oo[).1; first exact: closure_subset. + exact: rray_closed. +rewrite -itvoy_closureE//. +by apply/closure_subset/subset_itv => //; rewrite !bnd_simp. +Qed. + +Let itvNyo_closureE (x : T) : + is_endless_porderType T -> is_dense_porderType T -> + closure `]-oo, x[ = `]-oo, x]. +Proof. +move=> T_endless T_dense. +have subcy : `]-oo, x[ `<=` `]-oo, x]. + by apply: subset_itv => //; rewrite !bnd_simp. +apply/seteqP; split. + rewrite (closure_id `]-oo, x]).1; first exact: closure_subset. + exact: lray_closed. +rewrite (closureEbigcap_itvcc `]-oo, x])//; last exact: lray_closed. +rewrite setorder_itv_setDl_image// setDcitvNy; last first. + by apply/set0P; exists x; rewrite /= in_itv/= lexx. +rewrite powerset1 image_setU !image_set1 setD0 setDitv1r setIC setIUl. +move=> /= z/= zx /= i [] [] -> // ci; exfalso. +move/closed_itv_closed_ends: ci; cbn; rewrite falseE; apply => //. +have[[y yx] _]:= T_endless x. +by apply/set0P; exists y; rewrite /= in_itv/= yx. +Qed. + +Lemma linfty_itv_closureE (x : T) b : + is_endless_porderType T -> is_dense_porderType T -> + closure [set` Interval -oo (BSide b x)] = `]-oo, x]. +Proof. +move=> T_endless T_dense. +have subNyc: [set` Interval -oo (BSide b x)] `<=` `]-oo, x]. + by apply: subset_itv => //; rewrite !bnd_simp. +apply/seteqP; split. + rewrite (closure_id `]-oo, x]).1; first exact: closure_subset. + exact: lray_closed. +rewrite -itvNyo_closureE//. +by apply/closure_subset/subset_itv => //; rewrite !bnd_simp. +Qed. + +Lemma rinfty_itv_interiorE (x : T) b : + is_endless_porderType T -> is_dense_porderType T -> + [set` Interval (BSide b x) +oo]° = `]x, +oo[. +Proof. +move=> T_endless T_dense. +by apply: setC_inj; rewrite -closure_setC !setCitvr linfty_itv_closureE. +Qed. + +Lemma linfty_itv_interiorE (x : T) b : + is_endless_porderType T -> is_dense_porderType T -> + [set` Interval -oo (BSide b x)]° = `]-oo, x[. +Proof. +move=> T_endless T_dense. +by apply: setC_inj; rewrite -closure_setC !setCitvl rinfty_itv_closureE. +Qed. + +Lemma fin_itv_interiorE (x y : T) b1 b2 : + is_endless_porderType T -> is_dense_porderType T -> + [set` Interval (BSide b1 x) (BSide b2 y)]° = `]x, y[. +Proof. +move=> T_endless T_dense. +apply: setC_inj. +rewrite -closure_setC !setCitv/= closureU. +by rewrite linfty_itv_closureE// rinfty_itv_closureE. +Qed. + +Lemma itv_closureE (l r : itv_bound T) : + is_endless_porderType T -> is_dense_porderType T -> + [set` Interval l r] != set0 -> + closure [set` Interval l r] = + [set` Interval + (match l with BSide _ x => BLeft x | BInfty _ => l end) + (match r with BSide _ y => BRight y | BInfty _ => r end)]. +Proof. +move=> T_endless T_dense. +case: l => [b1 x | b1]; case: r => [b2 y | b2]; case: b1; case: b2 => ineq0. +all: rewrite ?set_itv_infty_set0 ?closure0//. +all: rewrite ?set_itvNyy ?closureT//. +all: by rewrite (fin_itv_closureE, rinfty_itv_closureE, linfty_itv_closureE). +Qed. + +Lemma itv_interiorE (l r : itv_bound T) : + is_endless_porderType T -> is_dense_porderType T -> + [set` Interval l r]° = + [set` Interval + (match l with BSide _ x => BRight x | BInfty _ => l end) + (match r with BSide _ y => BLeft y | BInfty _ => r end)]. +Proof. +move=> T_endless T_dense. +case: l => [b1 x | b1]; case: r => [b2 y | b2]; case: b1; case: b2. +all: rewrite ?set_itv_infty_set0 ?interior0//. +all: rewrite ?set_itvNyy ?interiorT//. +all: by rewrite (fin_itv_interiorE, rinfty_itv_interiorE, linfty_itv_interiorE). +Qed. + +End theory. + +End EndlessDenseOrderTopologyTheory. + +Section realField_topology. +Variable R : realFieldType. +Local Open Scope order_scope. + +Let real_is_endless := @EndlessDenseOrderTheory.numDomain_is_endless R. +Let real_is_dense := @EndlessDenseOrderTheory.numField_is_dense R. + +Lemma open_itv_open_ends (i : interval R) : + [set` i] != set0 -> open [set` i] -> itv_open_ends i. +Proof. exact: EndlessDenseOrderTopologyTheory.open_itv_open_ends. Qed. + +Lemma closed_itv_closed_ends (i : interval R) : + [set` i] != set0 -> closed [set` i] -> itv_closed_ends i. +Proof. exact: EndlessDenseOrderTopologyTheory.closed_itv_closed_ends. Qed. + +Lemma itv_closureE (l r : itv_bound R) : + [set` Interval l r] != set0 -> + closure [set` Interval l r] = + [set` Interval + (match l with BSide _ x => BLeft x | BInfty _ => l end) + (match r with BSide _ y => BRight y | BInfty _ => r end)]. +Proof. exact: EndlessDenseOrderTopologyTheory.itv_closureE. Qed. + +Lemma itv_interiorE (l r : itv_bound R) : + [set` Interval l r]° = + [set` Interval + (match l with BSide _ x => BRight x | BInfty _ => l end) + (match r with BSide _ y => BLeft y | BInfty _ => r end)]. +Proof. exact: EndlessDenseOrderTopologyTheory.itv_interiorE. Qed. + +End realField_topology. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 58e897bd0..129b4006b 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -923,6 +923,46 @@ apply: eq_bigcapl; split => X /=. by case=> Y + <-; rewrite closedC setCS. Qed. +Lemma closureEbigcap_itvcy A : + closure A = \bigcap_(x in closed `&` `[A, +oo[) x. +Proof. +rewrite closureEbigcap; apply: eq_bigcapl. +by split => ? /=; rewrite in_itv/= -subsetEset andbT. +Qed. + +Lemma interiorEbigcup_itvNyc A : + A° = \bigcup_(x in open `&` `]-oo, A]) x. +Proof. +apply: setC_inj; rewrite -closure_setC closureEbigcap_itvcy setC_bigcup. +rewrite -[RHS](bigcap_image _ setC); apply: eq_bigcapl. +apply/seteqP/funext => X. +rewrite -(setCK X) image_inj; last exact: setC_inj. +by rewrite /= !in_itv/= andbT !subsetEset setCS setCK openC. +Qed. + +Lemma closureEbigcap_itvcc A B : + closed B -> A `<=` B -> closure A = \bigcap_(x in closed `&` `[A, B]) x. +Proof. +move=> cB; rewrite -subsetEset => AB. +rewrite closureEbigcap_itvcy /bigcap; apply/seteqP. +split => x /= H Y [] cY; rewrite in_itv/= => /andP[] AY YB. + by have:= H Y; apply; split => //; rewrite in_itv/= AY. +apply/(@subIsetl _ _ B)/(H (Y `&` B)); split; first exact: closedI. +rewrite in_itv/=; apply/andP. +by rewrite Order.MeetTheory.lexI Order.MeetTheory.leIr AY AB. +Qed. + +Lemma interiorEbigcup_itvcc A B : + open B -> B `<=` A -> A° = \bigcup_(x in open `&` `[B, A]) x. +Proof. +rewrite -closedC -subsetCP => cB AB. +apply: setC_inj; rewrite -closure_setC (closureEbigcap_itvcc cB AB) setC_bigcup. +rewrite -[RHS](bigcap_image _ setC); apply: eq_bigcapl. +apply/seteqP/funext => X. +rewrite -(setCK X) image_inj; last exact: setC_inj. +by rewrite /= !in_itv/= !Order.CTBDistrLatticeTheory.leC setCK openC andbC. +Qed. + Lemma interior_closed_regopen A : closed A -> regopen A°. Proof. move=> cA; rewrite /regopen eqEsubset; split=> x. @@ -952,6 +992,9 @@ Proof. move=> ?; exact/closure_open_regclosed/open_interior. Qed. End closure_interior_lemmas. +Arguments closureEbigcap_itvcc {T A}. +Arguments interiorEbigcup_itvcc {T A}. + Lemma closureC_deprecated (T : topologicalType) (E : set T) : ~` closure E = \bigcup_(x in [set U | open U /\ U `<=` ~` E]) x. Proof. by rewrite -interiorC interiorEbigcup. Qed. From bdf9839feab79b702dcd91cc731bfac65cd22908 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Tue, 17 Feb 2026 11:30:15 +0900 Subject: [PATCH 2/2] clean and use neitv --- classical/set_interval.v | 22 +++++++++----------- classical/unstable.v | 1 - theories/topology_theory/num_topology.v | 27 ++++++++++++------------- 3 files changed, 23 insertions(+), 27 deletions(-) diff --git a/classical/set_interval.v b/classical/set_interval.v index 1645fb144..02f585413 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -55,10 +55,7 @@ Implicit Types (i j : interval T) (x y : T) (a : itv_bound T). Definition neitv i := [set` i] != set0. Lemma neitv_lt_bnd i : neitv i -> (i.1 < i.2)%O. -Proof. -case: i => a b; apply: contraNT => /= /itv_ge ab0. -by apply/eqP; rewrite predeqE => t; split => //=; rewrite ab0. -Qed. +Proof. case: i => a b /set0P[] ?; exact: itv_boundlr_lt. Qed. Lemma set_itvP i j : [set` i] = [set` j] :> set _ <-> i =i j. Proof. @@ -343,11 +340,11 @@ move=> cab; apply/seteqP; split => [x /= [xab /eqP]|x[|]]/=. Qed. Lemma setDitvoo (x y : T) (b1 b2 : bool) : - [set` Interval (BSide b1 x) (BSide b2 y)] != set0 -> + neitv (Interval (BSide b1 x) (BSide b2 y)) -> [set` Interval (BSide b1 x) (BSide b2 y)] `\` `]x, y[ = (if b1 then [set x] else set0) `|` (if b2 then set0 else [set y]). Proof. -case/set0P => u /= /itv_boundlr_lt xy. +move=> /neitv_lt_bnd/= xy. apply/seteqP; split => z/=; rewrite !in_itv/=; last first. move: b1 b2 xy. case=> -[]; rewrite !bnd_simp/= => + []// -> => ->; rewrite ?lexx ?ltxx//. @@ -362,11 +359,11 @@ case=> -[]/= + /andP[]; rewrite ?ltNge !negbK => /orP[]; try move=> -> //. Qed. Lemma setDccitv (x y : T) (b1 b2 : bool) : - `[x, y]%classic != set0 -> + neitv `[x, y] -> `[x, y] `\` [set` Interval (BSide b1 x) (BSide b2 y)] = (if b1 then set0 else [set x]) `|` (if b2 then [set y] else set0). Proof. -case/set0P => u /= /itv_boundlr_lt xy. +move=> /neitv_lt_bnd/= xy. apply/seteqP; split => z/=; rewrite !in_itv/=; last first. move: b1 b2 xy. case=> -[]; rewrite !bnd_simp/= => + []// -> => ->; rewrite ?lexx ?ltxx//. @@ -381,7 +378,7 @@ case=> -[]/= /orP[] + /andP[]; rewrite -?leNgt; try move=> /negPf -> //. Qed. Lemma setDitvoy a (x : T) (b : bool) : - [set` Interval (BSide b x) a] != set0 -> + neitv (Interval (BSide b x) a) -> [set` Interval (BSide b x) a] `\` `]x, +oo[ = (if b then [set x] else set0). Proof. @@ -394,7 +391,7 @@ by case=> /andP[] ? _ /negP; rewrite -leNgt => ?; apply/le_anti/andP; split. Qed. Lemma setDitvNyo a (x : T) (b : bool) : - [set` Interval a (BSide b x)] != set0 -> + neitv (Interval a (BSide b x)) -> [set` Interval a (BSide b x)] `\` `]-oo, x[ = (if b then set0 else [set x]). Proof. @@ -407,7 +404,7 @@ by case=> /andP[] _ ? /negP; rewrite -leNgt => ?; apply/le_anti/andP; split. Qed. Lemma setDcitvy a (x : T) (b : bool) : - [set` Interval (BLeft x) a] != set0 -> + neitv (Interval (BLeft x) a) -> [set` Interval (BLeft x) a] `\` [set` Interval (BSide b x) +oo%O] = (if b then set0 else [set x]). Proof. @@ -420,9 +417,10 @@ by case=> /andP[] ? _ /negP; rewrite -leNgt => ?; apply/le_anti/andP; split. Qed. Lemma setDcitvNy a (x : T) (b : bool) : - [set` Interval a (BRight x)] != set0 -> + neitv (Interval a (BRight x)) -> [set` Interval a (BRight x)] `\` [set` Interval -oo%O (BSide b x)] = (if b then [set x] else set0). +Proof. case/set0P => u xau. apply/seteqP; split => z/=; rewrite !in_itv/=; last first. move: xau; case: b; rewrite //= => /[swap] <-. diff --git a/classical/unstable.v b/classical/unstable.v index ed7109560..387315c2c 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -571,7 +571,6 @@ Module EndlessDenseOrderTheory. Section theory. Local Open Scope order_scope. -(*Local Open Scope classical_set_scope.*) Definition is_endless_porderType {d} (T : porderType d) := forall x : T, (exists y, y < x) /\ (exists y, x < y). diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index 3f70fe910..db9ef07f0 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -506,11 +506,11 @@ Context {d} {T : orderTopologicalType d}. Implicit Types x y : T. Lemma open_itv_open_ends (i : interval T) : - is_endless_porderType T -> is_dense_porderType T -> [set` i] != set0 -> + is_endless_porderType T -> is_dense_porderType T -> neitv i -> open [set` i] -> itv_open_ends i. Proof. move=> T_endless T_dense. -case: i => l r /set0P[?/=] /itv_boundlr_lt lr. +case: i => l r /neitv_lt_bnd/= lr. rewrite openE /interior/=. (under [X in X -> _]eq_forall do rewrite itv_nbhsE/=) => i_open. apply/negbNE/negP; case/(itv_open_endsPn lr) => x lrx. @@ -527,11 +527,11 @@ by case: lrx => <-; [left|right]; apply/le_anti/andP; split. Qed. Lemma closed_itv_closed_ends (i : interval T) : - is_endless_porderType T -> is_dense_porderType T -> [set` i] != set0 -> + is_endless_porderType T -> is_dense_porderType T -> neitv i -> closed [set` i] -> itv_closed_ends i. Proof. move=> T_endless T_dense. -case: i => l r /set0P[?/=] /itv_boundlr_lt lr. +case: i => l r /neitv_lt_bnd/= lr. rewrite closedE/= /prop_near1/=. (under [X in X -> _]eq_forall do rewrite itv_nbhsE/=) => i_closed. apply/negbNE/negP; case/(itv_closed_endsPn lr) => x lrx. @@ -556,11 +556,11 @@ by have := ly; rewrite ge_max => /andP[]. Qed. Let itvoo_closureE (x y : T) : - is_endless_porderType T -> is_dense_porderType T -> `]x, y[ != set0 -> + is_endless_porderType T -> is_dense_porderType T -> neitv `]x, y[%O -> closure `]x, y[ = `[x, y]. Proof. -move=> T_endless T_dense /set0P[] u /itv_boundlr_lt /[!bnd_simp] xy. -have ineq0 bb1 bb2 : [set` Interval (BSide bb1 x) (BSide bb2 y)] != set0. +move=> T_endless T_dense /neitv_lt_bnd/= /[!bnd_simp] xy. +have ineq0 bb1 bb2 : neitv (Interval (BSide bb1 x) (BSide bb2 y)). have[z /andP[xz zy]]:= T_dense x y xy. apply/set0P; exists z; rewrite /= in_itv/=. by case: bb1; case: bb2; apply/andP; split; rewrite /= ?ltW. @@ -578,10 +578,10 @@ Qed. Lemma fin_itv_closureE (x y : T) b1 b2 : is_endless_porderType T -> is_dense_porderType T -> - [set` Interval (BSide b1 x) (BSide b2 y)] != set0 -> + neitv (Interval (BSide b1 x) (BSide b2 y)) -> closure [set` Interval (BSide b1 x) (BSide b2 y)] = `[x, y]. Proof. -move=> T_endless T_dense /set0P[] u /= /itv_boundlr_lt bxy. +move=> T_endless T_dense /neitv_lt_bnd/= bxy. have : x <= y by move: bxy; case: b1; case: b2; rewrite bnd_simp// => /ltW. rewrite le_eqVlt => /orP[/eqP xy| xy]. move: b1 b2 bxy; rewrite xy => -[][]; rewrite !bnd_simp// => _. @@ -690,8 +690,7 @@ by rewrite linfty_itv_closureE// rinfty_itv_closureE. Qed. Lemma itv_closureE (l r : itv_bound T) : - is_endless_porderType T -> is_dense_porderType T -> - [set` Interval l r] != set0 -> + is_endless_porderType T -> is_dense_porderType T -> neitv (Interval l r) -> closure [set` Interval l r] = [set` Interval (match l with BSide _ x => BLeft x | BInfty _ => l end) @@ -730,15 +729,15 @@ Let real_is_endless := @EndlessDenseOrderTheory.numDomain_is_endless R. Let real_is_dense := @EndlessDenseOrderTheory.numField_is_dense R. Lemma open_itv_open_ends (i : interval R) : - [set` i] != set0 -> open [set` i] -> itv_open_ends i. + neitv i -> open [set` i] -> itv_open_ends i. Proof. exact: EndlessDenseOrderTopologyTheory.open_itv_open_ends. Qed. Lemma closed_itv_closed_ends (i : interval R) : - [set` i] != set0 -> closed [set` i] -> itv_closed_ends i. + neitv i -> closed [set` i] -> itv_closed_ends i. Proof. exact: EndlessDenseOrderTopologyTheory.closed_itv_closed_ends. Qed. Lemma itv_closureE (l r : itv_bound R) : - [set` Interval l r] != set0 -> + neitv (Interval l r) -> closure [set` Interval l r] = [set` Interval (match l with BSide _ x => BLeft x | BInfty _ => l end)