diff --git a/theories/evt.v b/theories/evt.v index e216ee4426..9501463cc4 100644 --- a/theories/evt.v +++ b/theories/evt.v @@ -100,7 +100,20 @@ HB.builders Context R E of TopologicalLmod_isEvt R E. Unshelve. all: by end_near. Qed. - + Lemma nbhs_scaler: forall (U : set E) (r : R) (x :E), ( + r != 0) -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U). + Proof. + move => U r x r0 U0; move: (@scale_continuous ((r^-1,r *:x)) U). + rewrite /= scalerA mulrC divrr ?scale1r ?unitfE //= =>/(_ U0). + case=>//= [B] [B1 B2] BU. + near=> z => //=. + exists (r^-1*:z). + apply: (BU (r^-1,z)); split => //=; last by near: z. + by apply: nbhs_singleton. + by rewrite scalerA divrr ?scale1r ?unitfE //=. + Unshelve. all: by end_near. + Qed. + Lemma nbhsT: forall (U : set E), forall (x : E), nbhs 0 U -> nbhs x (+%R x @`U). Proof. move => U x U0. @@ -156,26 +169,39 @@ Lemma nbhsE_subproof : nbhs = nbhs_ entourage. Proof. rewrite /nbhs_ /=; apply: funext => x; rewrite /filter_from /=. apply: funext => U; apply: propext => /=; rewrite /entourage /=; split. -move=> nU; exists [set xy | U(x + (xy.1 - xy.2))]. - exists ((fun z => z-x) @` U); split. - rewrite -(addrN x) addrC; move: (nbhs_add (-x) nU). - have -> : [set ((- x)%R + x0)%E | x0 in U] = [set z - x | z in U]. - apply: funext => z /=; apply: propext; split; - by move=> [x0 U0]; rewrite addrC=> H; exists x0. - by []. - move => xy; rewrite !inE /= => [[z] Uz ] <-. - by rewrite addrCA subrr addr0. -move => /= z. (*issue*) admit. + pose V := [set v | (x-v) \in U] : set E. + move=> nU; exists [set xy | (xy.1 - xy.2) \in V]. + exists V;split. + have lem: (-1 != (0 : R)). + (* apply/eqP=> A. apply (f_equal (fun (z :R) => z + 1)) in A. + move: A. rewrite addrC subrr add0r; apply/eqP. + move:(oner_eq0 R). rewrite (eqC 1 0). *) + admit. + move: (nbhs_add (x) (nbhs_scaler lem nU))=> /=. + rewrite scaleN1r subrr /= /V. + have -> : [set (x + x0)%E | x0 in [set -1 *: x | x in U]] + = [set v | x - v \in U]. + apply: funext => /= v /=; rewrite inE; apply: propext; split. + by move => [x0 [x1]] Ux1 <- <-; rewrite scaleN1r opprB addrCA subrr addr0. + move=> Uxy. exists (v - x). exists (x -v) => //. + by rewrite scaleN1r opprB. + by rewrite addrCA subrr addr0 //. + by []. + by move=> xy; rewrite !inE=> Vxy; rewrite /= !inE. + by move=> y; rewrite /V /= !inE /= opprB addrCA subrr addr0 inE. move=> [A [U0 [NU UA]] H]. near=> z; apply: H => /=; rewrite -inE; apply: UA => /=. near: z; rewrite nearE. -move: (nbhsT x NU)=> /=. -have -> : [set (x + x0)%E | x0 in U0] = (fun x0 : E => x - x0 \in U0). - apply:funext => z /=; rewrite inE; apply: propext; split. - move=> [x0 H <-]; rewrite -opprB -addrAC addrN add0r. - admit (*issue*). - move=> Uxz; exists (z-x). admit (*issue*). - by rewrite addrCA subrr addr0. +have lem: (-1 != (0 : R)). admit. +move: (nbhsT x (nbhs0_scaler lem NU))=> /=. +have -> : +[set (x + x0)%E | x0 in [set -1 *: x | x in U0]] = (fun x0 : E => x - x0 \in U0). + apply:funext => /= z /=; apply: propext; split. + move=> [x0] [x1 Ux1 <-] <-. + rewrite -opprB. rewrite addrAC subrr add0r inE scaleN1r opprK //. + rewrite inE => Uxz. exists (z-x). exists (x-z) => //. + by rewrite scalerBr !scaleN1r opprK addrC. + by rewrite addrCA subrr addr0. by []. Admitted.