# Zulip Chat Archive

## 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 the hypotheses are contradictory. 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, contradiction, } 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 -- Now we get this proof for free: 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 lt_of_le_of_lt (dist_triangle z x y) (add_lt_add_of_lt_of_le zx h) 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

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

@Kevin Buzzard Could we help you to write the tutorial?

#### 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?

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

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:39):

I don't know anything about this kind of maths

#### 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.

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

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)⟩`

.

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

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