Skip to content

Fixes 1931 #1932

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
affeldt-aist merged 2 commits into from
Apr 6, 2026
+10 −10
Merged

Fixes 1931 #1932

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b4ccdf4
fixes #1931
affeldt-aist Apr 6, 2026
d004ac1
fixes #1930
affeldt-aist Apr 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 9 additions & 9 deletions theories/normedtype_theory/normed_module.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1040,11 +1040,11 @@ split=> [Ea V aV|]; last first.
pose elt_prop (ar : R * R) := [/\ ball a ar.2 `<=` V,
ar.1 \in E, ar.1 \in (ball a ar.2 : set R), ar.2 > 0 & ar.1 != a].
pose elt_type := {ar : R * R | elt_prop ar}.
pose a_ (x : elt_type) := (proj1_sig x).2.
pose r_ (x : elt_type) := (proj1_sig x).1.
pose a_ (x : elt_type) := (proj1_sig x).1.
pose r_ (x : elt_type) := (proj1_sig x).2.
(* two successive (a_i, r_i) and (a_j, r_j) satisfy the relation: *)
pose elt_rel i j := `|a - r_ i| = a_ j /\ ball a (a_ j) `<=` ball a (a_ i) /\
`|a - r_ j| < `|a - r_ i| /\ r_ i != r_ j.
pose elt_rel i j := `|a - a_ i| = r_ j /\ ball a (r_ j) `<=` ball a (r_ i) /\
`|a - a_ j| < `|a - a_ i| /\ a_ i != a_ j.
move: aV => -[r0/= r0_gt0 ar0V].
pose V0 : set R := ball a r0.
move/limit_pointP : Ea => [y_ [y_E y_neq_a y_cvg_a]].
Expand All @@ -1056,7 +1056,7 @@ have [a0 [a0a a0V0 a0E]] : exists a0, [/\ a0 != a, a0 \in V0 & a0 \in E].
have [v [v0 Pv]] : {v : nat -> elt_type |
v 0 = exist _ (a0, r0) (And5 ar0V a0E a0V0 r0_gt0 a0a) /\
forall n, elt_rel (v n) (v n.+1)}.
apply: dependent_choice => -[[ai ri] [/= ariV xE aiari ri_gt0 aia]].
apply: dependent_choice => -[[ai ri] [/= ariV xE aiari ri_gt0 aia]].
pose rj : R := `|a - ai|.
have rj_gt0 : 0 < rj by rewrite /rj normr_gt0 subr_eq0 eq_sym.
apply/cid; move/cvgrPdist_lt : y_cvg_a => /(_ _ rj_gt0)[M/= _ May_rj].
Expand All @@ -1070,14 +1070,14 @@ have [v [v0 Pv]] : {v : nat -> elt_type |
have y_ME : y_ M \in E by rewrite inE; apply/y_E/imageT.
exists (exist _ (y_ M, rj) (And5 VjV y_ME y_MVj rj_gt0 (y_neq_a M))) => /=.
split; first exact.
split; rewrite /a_ /r_/=.
split; rewrite /r_ /a_/=.
by apply: le_ball; move: aiari; rewrite inE => /ltW.
split; first by move: y_MVj; rewrite inE.
by apply/eqP => aiyM; move: y_MVj; rewrite -aiyM inE /Vj /ball/= /rj ltxx.
apply/infiniteP/pcard_leP/injfunPex => /=; exists (r_ \o v).
move=> n _; rewrite /r_ /=.
apply/infiniteP/pcard_leP/injfunPex => /=; exists (a_ \o v).
move=> n _; rewrite /a_ /=.
by case: (v n) => -[ai ri] [/= ariV /set_mem Eai /set_mem/ariV aiari _ _].
have arv q p : (p < q)%N -> `|a - r_ (v q)| < `|a - r_ (v p)|.
have arv q p : (p < q)%N -> `|a - a_ (v q)| < `|a - a_ (v p)|.
elim: q p => [[]//|q ih p].
by rewrite ltnS leq_eqVlt => /predU1P[->|/ih]; last apply: lt_trans;
by case: (Pv q) => _ [] _ [].
Expand Down
2 changes: 1 addition & 1 deletion theories/topology_theory/topology_structure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -791,7 +791,7 @@ Lemma closed_closure (A : set T) : closed (closure A).
Proof. by move=> p clclAp B /nbhs_interior /clclAp [q [clAq /clAq]]. Qed.

End Closed.
#[deprecated(since="mathcomp-analysis 1.15.0", note="use `closure_limit_point_isolated` instead")]
#[deprecated(since="mathcomp-analysis 1.15.0", note="use `closure_isolated_limit_point` instead")]
Notation closure_limit_point := __deprecated__closure_limit_point (only parsing).

Lemma preimage_closed {T U : topologicalType} (f : T -> U) (D : set U) :
Expand Down
Loading