lemma about !=set0 (#1768)

* lemma about !=set0

---------

Co-authored-by: IshiguroYoshihiro <[email protected]>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `classical_sets.v`:
+  + lemma `nonemptyPn`
+
 - in `cardinality.v`:
   + lemma `infinite_setD`
 

classical/classical_sets.v

@@ -834,6 +834,9 @@ apply: contrapT => /asboolPn/forallp_asboolPn A0; apply/A_neq0/eqP.
 by rewrite eqEsubset; split.
 Qed.
 
+Lemma nonemptyPn 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/nonemptyPn. 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; exact/nonemptyPn. Qed.
 
 Lemma has_sup1 x : has_sup [set x].
 Proof. by split; [exists x | exists x => y ->]. Qed.
@@ -2992,10 +2995,10 @@ Lemma has_inf1 x : has_inf [set x].
 Proof. by split; [exists x | exists x => y ->]. Qed.
 
 Lemma subset_has_lbound A B : A `<=` B -> has_lbound B -> has_lbound A.
-Proof. by move=> AB [l Bl]; exists l => a Aa; apply/Bl/AB. Qed.
+Proof. by move=> AB [l Bl]; exists l => a Aa; exact/Bl/AB. Qed.
 
 Lemma subset_has_ubound A B : A `<=` B -> has_ubound B -> has_ubound A.
-Proof. by move=> AB [l Bl]; exists l => a Aa; apply/Bl/AB. Qed.
+Proof. by move=> AB [l Bl]; exists l => a Aa; exact/Bl/AB. Qed.
 
 Lemma downP A x : (exists2 y, A y & (x <= y)%O) <-> down A x.
 Proof. by split => [[y Ay xy]|[y [Ay xy]]]; [exists y| exists y]. Qed.
@@ -3118,7 +3121,6 @@ Fact set_display : Order.disp_t. Proof. by []. Qed.
 Module SetOrder.
 Module Internal.
 Section SetOrder.
-
 Context {T : Type}.
 Implicit Types A B : set T.
 
@@ -3147,7 +3149,7 @@ HB.instance Definition _ :=
     joinKI meetKU (@setIUl _) setIid.
 
 Lemma SetOrder_sub0set A : (set0 <= A)%O.
-Proof. by apply/asboolP; apply: sub0set. Qed.
+Proof. by apply/asboolP; exact: sub0set. Qed.
 
 Lemma SetOrder_setTsub A : (A <= setT)%O.
 Proof. exact/asboolP. Qed.

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/nonemptyPn => -[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).

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/nonemptyPn => -[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.

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 [//|/nonemptyPn] := 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).

theories/topology_theory/connected.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2025 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 topology_structure.
@@ -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 /nonemptyPn]; case: b => ->;
     rewrite !(setU0,set0U); [left|right]; apply: subIset; right.
 case/not_andP => /eqP/set0P[x []].
 - move=> /closureI[cCx cAx] [Cx Bx]; exfalso.

theories/topology_theory/separation_axioms.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap.
 From mathcomp Require Import boolp classical_sets functions wochoice.
@@ -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] /nonemptyPn.
   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 =

theories/topology_theory/subspace_topology.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2025 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 topology_structure uniform_structure compact .
@@ -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/nonemptyPn => -[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.

theories/topology_theory/subtype_topology.v

@@ -1,3 +1,4 @@
+(* mathcomp analysis (c) 2025 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 reals topology_structure uniform_structure compact.