-
Notifications
You must be signed in to change notification settings - Fork 299
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.
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 by Bors] - feat(topology/uniform_space): some basic lemmas #3123
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't mind having lemmas using symmetric uniformities. I just have two minor comments.
bors d+
@@ -461,6 +502,25 @@ lemma ball_eq_of_symmetry {V : set (β × β)} (hV : symmetric_rel V) {x} : | |||
ball x V = {y | (y, x) ∈ V} := | |||
by { ext y, rw mem_ball_symmetry hV, exact iff.rfl } | |||
|
|||
lemma mem_comp_of_mem_ball {V W : set (β × β)} {x y z : β} (hV : symmetric_rel V) | |||
(hx : x ∈ ball z V) (hy : y ∈ ball z W) : (x, y) ∈ V ○ W := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(hx : x ∈ ball z V) (hy : y ∈ ball z W) : (x, y) ∈ V ○ W := | |
(hx : x ∈ ball z V) (hy : y ∈ ball z W) : (x, y) ∈ V ○ W := |
exact mem_sets_of_superset r_in r_sub, } | ||
end | ||
|
||
lemma uniformity_has_basis_closure : has_basis (𝓤 α) (λ V : set (α × α), V ∈ 𝓤 α) closure := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A docstring on this one would be welcome, as the has_basis ... closure
is surprising at first, before one tries to remember what has_basis
really says.
✌️ PatrickMassot can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
This is the second PR on the road to Heine. It contains various elementary lemmas about uniform spaces.
Pull request successfully merged into master. Build succeeded: |
…#3123) This is the second PR on the road to Heine. It contains various elementary lemmas about uniform spaces.
This is the second PR on the road to Heine. It contains various elementary lemmas about uniform spaces.
This PR is slightly controversial. You won't notice if you only look at the diff, but some of those lemmas are almost duplicating existing lemmas. This is because I'm returning to Bourbaki instead of following Johannes. The main differences are Johannes loves
filter.lift'
and he doesn't like symmetric entourages. So some lemmas from this PR are expressed withoutlift'
but have the same mathematical content as existing lemmas usinglift'
and some lemmas from this PR are symmetric versions of existing lemmas.