Skip to content

within_continuous_withinNx #1708

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
merged 3 commits into from
Sep 13, 2025
Merged

within_continuous_withinNx #1708

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
635a275
within_continuous_withinNx
Tragicus Aug 23, 2025
6f3e3f5
use contra_neq
affeldt-aist Sep 12, 2025
a33e561
rename within_continuous_withinNx to continuous_injective_withinNx
Tragicus Sep 12, 2025
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
3 changes: 3 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,9 @@
- in `num_normedtype.v`:
+ lemma `nbhs_infty_gtr`

- in `uniform_structure.v`:
+ lemma `continuous_injective_withinNx`

### Changed

- in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
Expand Down
12 changes: 12 additions & 0 deletions theories/topology_theory/uniform_structure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -284,6 +284,18 @@ rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].
Unshelve. all: by end_near. Qed.

Lemma continuous_injective_withinNx
(T U : topologicalType) (f : T -> U) (x : T) :
{for x, continuous f} ->
(forall y, f y = f x -> y = x) -> f @ x^' --> (f x)^'.
Proof.
move=> cf fI A; rewrite /nbhs /= /dnbhs !withinE/= => -[V Vfx AV].
exists (f @^-1` V); first exact: cf Vfx.
by apply/seteqP; split=> y/=;
move/predeqP : AV => /(_ (f y))/= AV [AVfy yx];
have /contra_neq /(_ yx) := fI y; tauto.
Qed.

(* This property is primarily useful for metrizability on uniform spaces *)
Definition countable_uniformity (T : uniformType) :=
exists R : set_system (T * T), [/\
Expand Down
Loading