We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 73f9982 commit 99c7a2aCopy full SHA for 99c7a2a
theories/borel_hierarchy.v
@@ -111,16 +111,16 @@ case:(px E cE) => f [] cf ->.
111
pose f' := f + cst (y - x).
112
exists f'.
113
split.
114
-rewrite /f'.
115
-move=> z.
116
-apply: continuousD.
117
-exact:cf.
118
-exact:cst_continuous.
+ rewrite /f'.
+ move=> z.
+ apply: continuousD.
+ exact:cf.
+ exact:cst_continuous.
119
apply/seteqP.
120
rewrite /f' /cst /=.
121
split => z /=.
122
-rewrite addrfctE => ->.
123
-by rewrite subrKC.
+ rewrite addrfctE => ->.
+ by rewrite subrKC.
124
rewrite addrfctE.
125
move/eqP.
126
by rewrite eq_sym -subr_eq opprB subrKC eq_sym => /eqP.
0 commit comments