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 `not_nonemptyP`
+
 - 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 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.

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).

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.

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).

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.

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 =

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.