Skip to content
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

Jump to bottom

[Merged by Bors] - feat (Topology/EMetricSpace): ext lemmas for Extended metric classes #10813

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat (Topology/EMetricSpace): ext lemmas for Extended metric classes #10813

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
64ad2f4
adding ext lemmas for Extended metric classes
Feb 21, 2024
05c3fae
applying feedback
Mar 26, 2024
1893b6a
now with no linter errors (hopefully)
Mar 26, 2024
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
20 changes: 20 additions & 0 deletions Mathlib/Topology/EMetricSpace/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ theorem uniformity_dist_of_mem_uniformity [LinearOrder β] {U : Filter (α × α
#align uniformity_dist_of_mem_uniformity uniformity_dist_of_mem_uniformity

/-- `EDist α` means that `α` is equipped with an extended distance. -/
@[ext]
class EDist (α : Type*) where
edist : α → α → ℝ≥0∞
#align has_edist EDist
Expand Down Expand Up @@ -89,6 +90,16 @@ attribute [instance] PseudoEMetricSpace.toUniformSpace

/- Pseudoemetric spaces are less common than metric spaces. Therefore, we work in a dedicated
namespace, while notions associated to metric spaces are mostly in the root namespace. -/

/-- Two pseudo emetric space structures with the same edistance function coincide. -/
@[ext]
protected theorem PseudoEMetricSpace.ext {α : Type*} {m m' : PseudoEMetricSpace α}
(h : m.toEDist = m'.toEDist) : m = m' := by
cases' m with ed _ _ _ U hU
cases' m' with ed' _ _ _ U' hU'
congr 1
exact UniformSpace.ext (((show ed = ed' from h) ▸ hU).trans hU'.symm)

variable [PseudoEMetricSpace α]

export PseudoEMetricSpace (edist_self edist_comm edist_triangle)
Expand Down Expand Up @@ -1015,6 +1026,15 @@ class EMetricSpace (α : Type u) extends PseudoEMetricSpace α : Type u where
eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
#align emetric_space EMetricSpace

@[ext]
protected theorem EMetricSpace.ext
{α : Type*} {m m' : EMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m' := by
cases m
cases m'
congr
ext1
assumption

variable {γ : Type w} [EMetricSpace γ]

export EMetricSpace (eq_of_edist_eq_zero)
Expand Down
Loading