Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Dec 28, 2023
1 parent 7dd785b commit 934eac6
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion theories/charge.v
Original file line number Diff line number Diff line change
Expand Up @@ -1373,7 +1373,7 @@ pose AP := A `&` P.
have mAP : measurable AP by exact: measurableI.
have muAP_gt0 : 0 < mu AP.
rewrite lt0e measure_ge0// andbT.
apply/eqP/(@contra_not _ _ (nu_mu _ mAP))/eqP; rewrite gt_eqF//.
apply/eqP/(contra_not (nu_mu _ mAP))/eqP; rewrite gt_eqF//.
rewrite (@lt_le_trans _ _ (sigma AP))//.
rewrite (@lt_le_trans _ _ (sigma A))//; last first.
rewrite (charge_partition _ _ mP mN)// gee_addl//.
Expand Down
2 changes: 1 addition & 1 deletion theories/topology.v
Original file line number Diff line number Diff line change
Expand Up @@ -3535,7 +3535,7 @@ Lemma open_hausdorff : hausdorff_space T =
[/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0].
Proof.
rewrite propeqE; split => [T_filterT2|T_openT2] x y.
have := @contra_not _ _ (T_filterT2 x y); rewrite (rwP eqP) (rwP negP). (* change @contra_not _ _ to contra_not when requiring MathComp > 1.14 *)
have := contra_not (T_filterT2 x y); rewrite (rwP eqP) (rwP negP).
move=> /[apply] /asboolPn/existsp_asboolPn[A]; rewrite -existsNE => -[B].
rewrite [nbhs _ _ -> _](rwP imply_asboolP) => /negP.
rewrite asbool_imply !negb_imply => /andP[/asboolP xA] /andP[/asboolP yB].
Expand Down

0 comments on commit 934eac6

Please sign in to comment.