Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Feb 18, 2025
1 parent fa9255e commit 20ed021
Showing 1 changed file with 4 additions and 6 deletions.
10 changes: 4 additions & 6 deletions theories/normedtype.v
Original file line number Diff line number Diff line change
Expand Up @@ -680,9 +680,8 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split.
move/(_ (F a - n%:R)) => [z [zreal zFan]].
exists `|ceil (z - a)|%N.
rewrite zFan// -ltrBlDl.
apply: (le_lt_trans (le_ceil _)).
apply: (le_lt_trans (ler_norm _)).
by rewrite -natr1 -intr_norm ltrDl.
rewrite (le_lt_trans (Num.Theory.le_ceil _)) ?num_real//.
by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl.
by exists i => //=; rewrite in_itv/= yFa (lt_le_trans _ Fany).
- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa].
exists `|ceil (F (a + n.+1%:R) - F a)%R|.+1 => //=.
Expand Down Expand Up @@ -714,9 +713,8 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split.
move/(_ (F a - n%:R)) => [z [zreal zFan]].
exists `|ceil (a - z)|%N.
rewrite zFan// ltrBlDr -ltrBlDl.
apply: (le_lt_trans (le_ceil _)).
apply: (le_lt_trans (ler_norm _)).
by rewrite -natr1 -intr_norm ltrDl.
rewrite (le_lt_trans (Num.Theory.le_ceil _)) ?num_real//.
by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl.
by exists i => //=; rewrite in_itv/= yFa andbT (lt_le_trans _ Fany).
- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa].
exists `| ceil (F (a - n.+1%:R) - F a)%R |.+1 => //=.
Expand Down

0 comments on commit 20ed021

Please sign in to comment.