## Stream: new members

### Topic: WIP: metric spaces tutorial

#### Kevin Buzzard (Apr 06 2020 at 18:13):

I've spent a few hours today trying to knock a metric spaces tutorial into shape because @Ryan Lahfa , @Jason KY. and @Kevin Doran were all independently formalising stuff like this. But I ran into trouble when I got to open sets because to manipulate open sets you need to be able to manipulate sets. So I think we need to roll back a bit and do a basic tutorial about working with sets. Here's how far I got with metric spaces (but as I say we need another tutorial first I think).

--import data.set
--import data.set.finite
import data.real.basic
--import data.finset
--import order.conditionally_complete_lattice
import topology.opens -- remove when finished checking types of things.
-- note: we don't import topology.metric_space.basic, which is
-- mathlib's version of metric spaces

/-! -/
--open_locale classical

open set

/-- A metric space is a set/type X equipped with a real-valued distance function
satisfying the usual axioms -/
class metric_space (X : Type) :=
(dist : X → X → ℝ)
(dist_self : ∀ x : X, dist x x = 0)
(eq_of_dist_eq_zero : ∀ {x y : X}, dist x y = 0 → x = y)
(dist_comm : ∀ x y : X, dist x y = dist y x)
(dist_triangle : ∀ x y z : X, dist x z ≤ dist x y + dist y z)

-- Exercise: compare with the definition in all the maths books.
-- Did we leave something out?

-- theorems that we are about to prove about metric spaces go in the metric space namespace
namespace metric_space

-- let X be a metric space
variables {X : Type} [metric_space X]

/-! # Learning to use linarith

We left out the axiom that ∀ x y : X, dist x y ≥ 0 in our metric space,
because it can be deduced from the triangle inequality and symmetry!
Let's prove it now, using linarith. The linarith tactic proves
many "obvious" results involving inequalities as long as the expressions
involved have degree 1. It looks at the hypotheses and tries to prove
the goal. For example if h : 0 ≤ a + a is a hypothesis, and the goal
is ⊢ 0 ≤ a, then linarith will close the goal.

Other useful tactics :

have h := dist_triangle x y x will create a new hypothesis h.

push_neg will move ¬ as far to the right as it can, and possibly
remove it. For example if h : ¬ (a ≤ b) then push_neg at h will change h to b < a.

by_contra h will create a hypothesis h saying that the goal is false, and
will replace the goal with false. Note that linarith can even prove a goal false if

Let's prove some basic things about distances using linarith.

-/

theorem dist_nonneg : ∀ (x y : X), 0 ≤ dist x y :=
begin
--replace with sorry in tutorial
intros x y,
have h := dist_triangle x y x,
rw dist_self at h,
rw dist_comm y x at h,
linarith,
end

theorem dist_le_zero {x y : X} : dist x y ≤ 0 ↔ x = y :=
begin
--replace with sorry in tutorial
split,
{ intro h,
have h2 := dist_nonneg x y,
apply eq_of_dist_eq_zero,
linarith,
},
{ intro h,
rw h,
rw dist_self,
}
end

theorem dist_pos {x y : X} : 0 < dist x y ↔ x ≠ y :=
begin
--replace with sorry in tutorial
split,
{ intro h,
intro hxy,
rw ←dist_le_zero at hxy,
linarith,
},
{ intro h,
by_contra h2,
push_neg at h2,
rw dist_le_zero at h2,

}
end

/-! ### Open balls

We define ball x ε to be the open ball centre x and radius ε. Note that we do not
require ε > 0! That hypothesis shows up later in the theorems, not in the definition.

-/

variables {x y z : X} {ε ε₁ ε₂ : ℝ} {s : set X}

/-- ball x ε is the set of all points y with dist y x < ε -/
def ball (x : X) (ε : ℝ) : set X := {y | dist y x < ε}

-- Let's tag this lemma with the simp tag, so the simp tactic will use it.
@[simp] theorem mem_ball : y ∈ ball x ε ↔ dist y x < ε := iff.rfl -- true by definition

theorem mem_ball_comm : x ∈ ball y ε ↔ y ∈ ball x ε :=
begin
simp [dist_comm]
end

-- Let's tag dist_self with the simp tag too:

attribute [simp] dist_self

-- Can you find a proof of this? And then can you find a one-line proof using simp?
theorem mem_ball_self (h : 0 < ε) : x ∈ ball x ε :=
begin
--replace with sorry
rw mem_ball,
rw dist_self,
exact h,
end

/- Top tip: rw mem_ball at hy ⊢ will rewrite mem_ball at both the hypothesis hy and the goal.
Get ⊢ in VS Code with \|-

-/
theorem ball_mono (h : ε₁ ≤ ε₂) : ball x ε₁ ⊆ ball x ε₂ :=
begin
-- delete me
intros y hy,
rw mem_ball at hy ⊢,
linarith,
end

/-! # Open sets.

A subset of a metric space is open if for every element s in the subset, there's some open
ball ball s ε, with ε > 0, entirely contained with S.
-/

/-- A subset U of a metric space is open if every s ∈ U there's an open ball centre s within U -/
def is_open (U : set X) := ∀ s ∈ U, ∃ (ε : ℝ) (hε : 0 < ε), ball s ε ⊆ U

-- Note that is_open is a Proposition. Things like is_open_Union below are proofs.

-- Let's start with two easy facts about open sets -- the empty set and the whole space is open.
theorem is_open_empty : is_open (∅ : set X) :=
begin
intro x,
intro hx,
cases hx,-- too hard for a beginner. Need to get a contradiction from h : x ∈ ∅
end

theorem is_open_univ : is_open (univ : set X) :=
begin
intro x,
intro hx,
use 37,
split,
norm_num,
-- need subset_univ
simp,
end

-- An arbitrary union of open sets is open. The union is indexed over an auxiliary type ι

-- TODO: I don't think this is any good, people need to know about set.subset.trans,
-- set.subset.Union etc. Should do something on sets first?

theorem is_open_Union (ι : Type) (f : ι → set X) (hf : ∀ (i : ι), is_open (f i)) :
is_open (⋃ (i : ι), f i) :=
begin
intro x,
intro hx,
rcases hx with ⟨U, ⟨i, rfl⟩, hxU⟩,
have h := hf i x hxU,
rcases h with ⟨ε, hε, hxε⟩,
use ε,
split, use hε,
refine set.subset.trans hxε _,
apply set.subset_Union,
end

theorem is_open_inter {U V : set X}  (hU : is_open U) (hV : is_open V) : is_open (U ∩ V) := sorry

/- A subset S of a metric space is closed if its complement is open -/
def is_closed (S : set X) := is_open (-S)

end metric_space

#exit

-- the lemmas from 274 to 300:
theorem closed_ball_subset_closed_ball {α : Type u} [metric_space α] {ε₁ ε₂ : ℝ} {x : α} (h : ε₁ ≤ ε₂) :
closed_ball x ε₁ ⊆ closed_ball x ε₂ :=
λ y (yx : _ ≤ ε₁), le_trans yx h

theorem ball_disjoint (h : ε₁ + ε₂ ≤ dist x y) : ball x ε₁ ∩ ball y ε₂ = ∅ :=
eq_empty_iff_forall_not_mem.2 $λ z ⟨h₁, h₂⟩, not_lt_of_le (dist_triangle_left x y z) (lt_of_lt_of_le (add_lt_add h₁ h₂) h) theorem ball_disjoint_same (h : ε ≤ dist x y / 2) : ball x ε ∩ ball y ε = ∅ := ball_disjoint$ by rwa [← two_mul, ← le_div_iff' two_pos]

theorem ball_subset (h : dist x y ≤ ε₂ - ε₁) : ball x ε₁ ⊆ ball y ε₂ :=
λ z zx, by rw ← add_sub_cancel'_right ε₁ ε₂; exact

theorem ball_half_subset (y) (h : y ∈ ball x (ε / 2)) : ball y (ε / 2) ⊆ ball x ε :=
ball_subset $by rw sub_self_div_two; exact le_of_lt h theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε := ⟨_, sub_pos.2 h, ball_subset$ by rw sub_sub_self⟩

theorem ball_eq_empty_iff_nonpos : ε ≤ 0 ↔ ball x ε = ∅ :=
(eq_empty_iff_forall_not_mem.trans
⟨λ h, le_of_not_gt $λ ε0, h _$ mem_ball_self ε0,
λ ε0 y h, not_lt_of_le ε0 \$ pos_of_mem_ball h⟩).symm

@[simp] lemma ball_zero : ball x 0 = ∅ :=
by rw [← metric.ball_eq_empty_iff_nonpos]

--

-- Do we want this?
theorem eq_of_forall_dist_le {x y : α} (h : ∀ε, ε > 0 → dist x y ≤ ε) : x = y :=
eq_of_dist_eq_zero (eq_of_le_of_forall_le_of_dense dist_nonneg h)

/-- The triangle (polygon) inequality for sequences of points; finset.range version. -/
lemma dist_le_range_sum_dist (f : ℕ → α) (n : ℕ) :
dist (f 0) (f n) ≤ (finset.range n).sum (λ i, dist (f i) (f (i + 1))) :=
finset.Ico.zero_bot n ▸ dist_le_Ico_sum_dist f (nat.zero_le n)

-- From mathlib
https://github.com/leanprover-community/mathlib/blob/17632202cdf9682cea972e86437d32ac20c91b06/src/topology/basic.lean#L262-L319

def closure (s : set α) : set α := ⋂₀ {t | is_closed t ∧ s ⊆ t}


#### Kevin Buzzard (Apr 06 2020 at 18:15):

My plan was to prove that closure was a Galois insertion. This comes out quite nicely.

#### Ryan Lahfa (Apr 06 2020 at 18:16):

@Kevin Buzzard Wow! Didn't know about the ⊢ trick!

But definitely, a set tutorial would be awesome, I do some stuff which might not be considered optimal by Lean seniors :)

#### Kevin Buzzard (Apr 06 2020 at 18:16):

But others might want to try other things. Perhaps one should do a series of three things: first a basic thing on sets, and then something on open and closed sets including def of metric space, and then a third one on basic stuff with limits of sequences perhaps, or stick to the real numbers or whatever.

#### Ryan Lahfa (Apr 06 2020 at 18:18):

Kevin Buzzard said:

But others might want to try other things. Perhaps one should do a series of three things: first a basic thing on sets, and then something on open and closed sets including def of metric space, and then a third one on basic stuff with limits of sequences perhaps, or stick to the real numbers or whatever.

Proving Bolzano-Weierstrass as a final result would quite awesome I think, it's one of the most powerful & non-trivial theorems you first learn as an undergraduate in real analysis (in France, at least AFAIK).
(well, there is also Heine theorem on uniform continuity over closed bounded intervals, i.e. compacts)

#### Ryan Lahfa (Apr 06 2020 at 18:19):

But that would require sticking to real numbers, and this is still possible to revisit the result in a 4th section if even necessary

#### Kevin Buzzard (Apr 06 2020 at 18:32):

Sure, that's why I posted here.

#### Kevin Buzzard (Apr 06 2020 at 18:33):

Ideally we would push them all to the tutorial project. Building up to something like BW would be very cool and of course it's possible to do in Lean, but a beginner wouldn't be able to do it without some help.

#### Patrick Massot (Apr 06 2020 at 18:35):

You can push to branch in the tutorial repository (if you don't have enough access we can investigate).

#### Kevin Buzzard (Apr 06 2020 at 18:35):

oh so it's like mathlib for someone like me?

#### Patrick Massot (Apr 06 2020 at 18:36):

As I wrote yesterday, I plan do to the same thing with my first year course, which focuses entirely on real numbers. So I think you should keep it at metric space level, with special emphasis on:

• using structures and classes
• setting up a theory, including simp lemmas

neither of those points are covered in my first year stuff.

#### Kevin Buzzard (Apr 06 2020 at 18:37):

OK. What about handling sets in general, e.g. subset_union or whatever?

#### Patrick Massot (Apr 06 2020 at 18:38):

I don't have any of that.

#### Kevin Buzzard (Apr 06 2020 at 18:38):

OK so for now I'll think about basic stuff with subsets, and then general metric spaces.

#### Patrick Massot (Apr 06 2020 at 18:38):

My part will be about handling logical connective and various kinds of reasonning

#### Ryan Lahfa (Apr 06 2020 at 18:41):

Kevin Buzzard said:

OK so for now I'll think about basic stuff with subsets, and then general metric spaces.

It might be hard to do, but a classical final boss of set theory is Cantor-Bernstein-Schröder, it requires some help though for a beginner

#### Ryan Lahfa (Apr 06 2020 at 18:41):

(but it'd need to introduce injective, surjective, bijective stuff… Unsure if it is wise.)

#### Patrick Massot (Apr 06 2020 at 18:52):

I'm not sure that would teach much Lean at that point.

#### Ryan Lahfa (Apr 06 2020 at 18:54):

Well, there is also mathlib API to learn too

#### Ryan Lahfa (Apr 06 2020 at 18:54):

Documentation is pretty great (there are few pain points) so I'm not sure if that's necessary at all

#### Kevin Buzzard (Apr 06 2020 at 19:01):

If we're doing open sets then we need to show the users how to prove the axioms for a topology, and these proofs seem to rely on a basic understanding of how to manipulate sets

#### Patrick Massot (Apr 06 2020 at 19:05):

Yes, sure. I was specifically referring to Cantor-Bernstein.

#### Ryan Lahfa (Apr 06 2020 at 19:10):

Patrick Massot said:

Yes, sure. I was specifically referring to Cantor-Bernstein.

BTW, is Cantor Bernstein in mathlib?

#### Ryan Lahfa (Apr 06 2020 at 19:10):

(docs would benefit if we could search by alternative names of big theorems or look for a theorem and get its generalization, I should open an issue)

#### Patrick Massot (Apr 06 2020 at 19:13):

Did you really search?

#### Patrick Massot (Apr 06 2020 at 19:13):

There is a file name giving you a hint...

#### Johan Commelin (Apr 06 2020 at 19:13):

@Ryan Lahfa PRs that add alternative names to docstrings are very welcome! (And they will usually get merged before you can reload your page :wink:)

#### Ryan Lahfa (Apr 06 2020 at 19:14):

Patrick Massot said:

Did you really search?

I definitely searched for "Cantor" and "Cantor-Bernstein", but I should have searched for something else, I suppose, in set_theory and cardinals (?)

#### Ryan Lahfa (Apr 06 2020 at 19:15):

Johan Commelin said:

Ryan Lahfa PRs that add alternative names to docstrings are very welcome! (And they will usually get merged before you can reload your page :wink:)

Sounds something I can do :)

#### Patrick Massot (Apr 06 2020 at 19:16):

https://leanprover-community.github.io/mathlib_docs/set_theory/schroeder_bernstein.html

#### Ryan Lahfa (Apr 06 2020 at 19:16):

Ryan Lahfa said:

Patrick Massot said:

Did you really search?

I definitely searched for "Cantor" and "Cantor-Bernstein", but I should have searched for something else, I suppose, in set_theory and cardinals (?)

→ schroeder_bernstein :D — I should have searched for bernstein I guess ; in France, we call it Cantor-Bernstein

#### Ryan Lahfa (Apr 06 2020 at 19:18):

If I wanted to see where is Banach-Tarski-Hausdorff paradox, where would I expect to find it?

#### Johan Commelin (Apr 06 2020 at 19:29):

I don't think it's there yet. But I guess it would be somewhere in measure_theory/

#### Patrick Massot (Apr 06 2020 at 19:31):

That could be a fun project for you.

#### Ryan Lahfa (Apr 06 2020 at 19:38):

Patrick Massot said:

That could be a fun project for you.

Definitely :-)

#### David Wärn (Apr 06 2020 at 19:55):

Is there something like the Vitali set to show that not every set of reals is measurable?

Highly unlikely

#### Kevin Buzzard (Apr 06 2020 at 20:11):

They're not into examples in mathlib

#### Yury G. Kudryashov (Apr 06 2020 at 20:15):

git grep -i Vitali

#### Yury G. Kudryashov (Apr 06 2020 at 20:16):

It is in measure_theory/lebesgue_measure but it is in a comment, so possibly it doesn't work with current mathlib.

#### Yury G. Kudryashov (Apr 06 2020 at 20:17):

You can move it to examples and PR

#### Yury G. Kudryashov (Apr 06 2020 at 20:17):

Then move it back if you'll need it for some proof.

#### Ryan Lahfa (Apr 06 2020 at 20:31):

Johan Commelin said:

I don't think it's there yet. But I guess it would be somewhere in measure_theory/

I will need some isometry stuff, I see metric_space/isometry, but, is there any notion of orientation (direct/indirect) isometries?
I tried to grep for direct in the file but no result.

#### Johan Commelin (Apr 06 2020 at 20:40):

What is a direct/indirect isometry?

#### Ryan Lahfa (Apr 06 2020 at 20:45):

Johan Commelin said:

What is a direct/indirect isometry?

Oh, sorry, if $f : A \to B$ is an isometry between euclidean affine spaces, we say that $f$ is direct when the linear part of $f$ is of determinant 1, IIRC.

Basically, $f$ preserves the orientation of the space.

#### Johan Commelin (Apr 06 2020 at 20:45):

Aah, ok. In that case I knew the concept :lol:

#### Yury G. Kudryashov (Apr 06 2020 at 20:47):

Probably you'll need to define SO(n)

#### Yury G. Kudryashov (Apr 06 2020 at 20:48):

We have SL(n) in linear_algebra/special_linear_group

#### Ryan Lahfa (Apr 06 2020 at 20:53):

Johan Commelin said:

Aah, ok. In that case I knew the concept :lol:

I attempted the dangerous game of direct (without pun) translation from French to English :D

#### Ryan Lahfa (Apr 06 2020 at 20:53):

Yury G. Kudryashov said:

Probably you'll need to define SO(n)

Yes, I'll definitely need $\mathrm{SO}_n$

#### Yury G. Kudryashov (Apr 06 2020 at 21:03):

Then you'll deal with $SO_n$, not isometry.

#### Ryan Lahfa (Apr 06 2020 at 21:09):

Yury G. Kudryashov said:

Then you'll deal with $SO_n$, not isometry.

Definitely, but I need to glue $SO_n$ and isometry, right? At least, I just need to know that an element of $O_n$ is an isometry.

#### Yury G. Kudryashov (Apr 06 2020 at 21:09):

Yes, but you don't have to define "orientation preserving" for isometries.

Agreed

#### Yury G. Kudryashov (Apr 06 2020 at 21:11):

BTW, you'll need to redefine euclidean_space. Right now it is define somewhere in geometry/ to help defining manifolds, and it has sup-norm instead of an inner_product_space structure.

#### Yury G. Kudryashov (Apr 06 2020 at 21:15):

Something like instance [fintype n] : has_inner (n → real) := ⟨λ a b, finset.univ.sum (λ i, a i * b i)⟩.

Makes sense

#### Kevin Doran (Apr 06 2020 at 22:35):

As a token learner, I just thought I'd mention that a set tutorial would be much appreciated; I quickly ran into trouble trying to use sets of sets and I didn't find it obvious how to work with them by looking at mathlib etc.

#### Kevin Buzzard (Apr 06 2020 at 23:06):

I pushed some stuff onto a branch of the tutorial project. I need to do other things tomorrow/Wed but hopefully I'll get back to it Thurs. Feel free to help out with some examples or exercises. I thought it was worth figuring out exactly which tactics are needed to prove the set stuff, because the moment we're into metric spaces we're using linarith etc.

Last updated: May 14 2021 at 13:24 UTC