From 69e4959dcfbcf94ac8dc52cd7b6c15d4e609bc63 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 19 Nov 2025 17:16:36 +0900 Subject: [PATCH] lemma about !=set0 Co-authored-by: IshiguroYoshihiro --- CHANGELOG_UNRELEASED.md | 3 +++ classical/classical_sets.v | 9 ++++++--- theories/normedtype_theory/pseudometric_normed_Zmodule.v | 2 +- theories/normedtype_theory/urysohn.v | 2 +- theories/normedtype_theory/vitali_lemma.v | 2 +- theories/topology_theory/connected.v | 2 +- theories/topology_theory/separation_axioms.v | 5 ++--- theories/topology_theory/subspace_topology.v | 2 +- 8 files changed, 16 insertions(+), 11 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 64e39fd72f..38ccbac616 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,6 +4,9 @@ ### Added +- in `classical_sets.v`: + + lemma `not_nonemptyP` + - in `cardinality.v`: + lemma `infinite_setD` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 7f9233cbc7..f72e48dce5 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -834,6 +834,9 @@ apply: contrapT => /asboolPn/forallp_asboolPn A0; apply/A_neq0/eqP. by rewrite eqEsubset; split. Qed. +Lemma not_nonemptyP A : ~ (A !=set0) <-> A = set0. +Proof. by split; [|move=> ->]; move/set0P/negP; [move/negbNE/eqP|]. Qed. + Lemma setF_eq0 : (T -> False) -> all_equal_to (set0 : set T). Proof. by move=> TF A; rewrite -subset0 => x; have := TF x. Qed. @@ -1206,7 +1209,7 @@ Notation bigcupM1l := bigcupX1l (only parsing). Notation bigcupM1r := bigcupX1r (only parsing). Lemma set_cst {T I} (x : T) (A : set I) : - [set x | _ in A] = if A == set0 then set0 else [set x]. + [set x | _ in A] = if A == set0 then set0 else [set x]. Proof. apply/seteqP; split=> [_ [i +] <-|t]; first by case: ifPn => // /eqP ->. by case: ifPn => // /set0P[i Ai ->{t}]; exists i. @@ -2980,10 +2983,10 @@ Lemma has_ub_set1 x : has_ubound [set x]. Proof. by exists x; rewrite ub_set1. Qed. Lemma has_inf0 : ~ has_inf (@set0 T). -Proof. by rewrite /has_inf not_andP; left; apply/set0P/negP/negPn. Qed. +Proof. by rewrite /has_inf not_andP; left; exact/not_nonemptyP. Qed. Lemma has_sup0 : ~ has_sup (@set0 T). -Proof. by rewrite /has_sup not_andP; left; apply/set0P/negP/negPn. Qed. +Proof. by rewrite /has_sup not_andP; left; apply/not_nonemptyP. Qed. Lemma has_sup1 x : has_sup [set x]. Proof. by split; [exists x | exists x => y ->]. Qed. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 139a94e8d0..b8e06bd0de 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -418,7 +418,7 @@ Proof. rewrite ball_hausdorff => a b ab. have ab2 : 0 < `|a - b| / 2 by apply divr_gt0 => //; rewrite normr_gt0 subr_eq0. set r := PosNum ab2; exists (r, r) => /=. -apply/negPn/negP => /set0P[c] []; rewrite -ball_normE /ball_ => acr bcr. +apply/eqP/not_nonemptyP => -[c] []; rewrite -ball_normE /ball_ => acr bcr. have r22 : r%:num * 2 = r%:num + r%:num. by rewrite (_ : 2 = 1 + 1) // mulrDr mulr1. move: (ltrD acr bcr); rewrite -r22 (distrC b c). diff --git a/theories/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v index e8f7ed4f6c..6ff977929a 100644 --- a/theories/normedtype_theory/urysohn.v +++ b/theories/normedtype_theory/urysohn.v @@ -842,7 +842,7 @@ split. - by apply: bigcup_open => ? ?; exact: open_interior. - by move=> x ?; exists x => //; exact: nbhsx_ballx. - by move=> y ?; exists y => //; exact: nbhsx_ballx. -- apply/eqP/negPn/negP/set0P => -[z [[x Ax /interior_subset Axe]]]. +- apply/not_nonemptyP => -[z [[x Ax /interior_subset Axe]]]. case=> y By /interior_subset Bye; have nAy : ~ A y. by move: AB0; rewrite setIC => /disjoints_subset; exact. have nBx : ~ B x by move/disjoints_subset: AB0; exact. diff --git a/theories/normedtype_theory/vitali_lemma.v b/theories/normedtype_theory/vitali_lemma.v index e2219db5ff..ef49efa518 100644 --- a/theories/normedtype_theory/vitali_lemma.v +++ b/theories/normedtype_theory/vitali_lemma.v @@ -474,7 +474,7 @@ have [[j Dj BiBj]|] := move/forall2NP => H. have {}H j : (\bigcup_(i < n.+1) D i) j -> closure (B i) `&` closure (B j) = set0. - by have [//|/set0P/negP/negPn/eqP] := H j. + by have [//|/not_nonemptyP] := H j. have H_i : (H_ n (\bigcup_(i < n) D i)) i. split => // s Hs si; apply: H => //. by move: Hs => [m /= nm Dms]; exists m => //=; rewrite (ltn_trans nm). diff --git a/theories/topology_theory/connected.v b/theories/topology_theory/connected.v index dd94ecae42..2a809c55b5 100644 --- a/theories/topology_theory/connected.v +++ b/theories/topology_theory/connected.v @@ -91,7 +91,7 @@ move=> AB CAB; have -> : C = (C `&` A) `|` (C `&` B). rewrite predeqE => x; split=> [Cx|[] [] //]. by have [Ax|Bx] := CAB _ Cx; [left|right]. move/connectedP/(_ (fun b => if b then C `&` B else C `&` A)) => /not_and3P[]//. - by move/existsNP => [b /set0P/negP/negPn]; case: b => /eqP ->; + by move/existsNP => [b /not_nonemptyP]; case: b => ->; rewrite !(setU0,set0U); [left|right]; apply: subIset; right. case/not_andP => /eqP/set0P[x []]. - move=> /closureI[cCx cAx] [Cx Bx]; exfalso. diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index 37029013aa..a95bda9a56 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -128,7 +128,7 @@ have /compact_near_coveringP : compact (V `\` U). move=> /(_ _ (powerset_filter_from F) (fun W x => ~ W x))[]. move=> z [Vz ?]; have zE : x <> z by move/nbhs_singleton: nbhsU => /[swap] ->. have : ~ cluster F z by move: zE; apply: contra_not; rewrite clFx1 => ->. - case/existsNP=> C /existsPNP [D] FC /existsNP [Dz] /set0P/negP/negPn/eqP. + case/existsNP=> C /existsPNP [D] FC /existsNP [Dz] /not_nonemptyP. rewrite setIC => /disjoints_subset CD0; exists (D, [set W | F W /\ W `<=` C]). by split; rewrite //= nbhs_simpl; exact: powerset_filter_fromP. by case => t W [Dt] [FW] /subsetCP; apply; apply: CD0. @@ -140,8 +140,7 @@ Qed. Lemma compact_precompact (A : set T) : hausdorff_space -> compact A -> precompact A. Proof. -move=> h c; rewrite precompactE ( _ : closure A = A)//. -by apply/esym/closure_id; exact: compact_closed. +by move=> h c; rewrite precompactE -(closure_id _).1//; exact: compact_closed. Qed. Lemma open_hausdorff : hausdorff_space = diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index 4d332c8f35..493515d547 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/theories/topology_theory/subspace_topology.v @@ -620,7 +620,7 @@ have ? : f @` closure (AfE b) `<=` closure (E b). have /(@preimage_subset _ _ f) A0cA0 := @subset_closure _ (E b). by apply: subset_trans A0cA0; apply: subIset; right. by move/subset_trans; apply; exact: image_preimage_subset. -apply/eqP/negPn/negP/set0P => -[t [? ?]]. +apply/not_nonemptyP => -[t [AfEb AfENb]]. have : f @` closure (AfE b) `&` f @` AfE (~~ b) = set0. by rewrite fAfE; exact: subsetI_eq0 cEIE. by rewrite predeqE => /(_ (f t)) [fcAfEb] _; apply: fcAfEb; split; exists t.