## Stream: maths

### Topic: Topology - Beginner

#### Luca Gerolla (Jul 05 2018 at 19:35):

Hello, I am a beginner and I am trying to define a path (in particular a path from x to y on a topological space).
I am sorry for the (temporary) maths notation of topological spaces and definitions.
Not knowing the syntax/ best way to impose the conditions for the continuous function (f : I = [0,1] --> X) to be a path I thought of having a product lean X × (I → X) × Prop  as output.

This is my code:

import analysis.topology.continuity
import analysis.topology.topological_space
import analysis.topology.infinite_sum
import analysis.topology.topological_structures
import analysis.topology.uniform_space

open set filter lattice classical
universe u

-- ambient space
variable {X : Type*}
#check X
------ variable x : X

-- topological space (X, T)
variable T : topological_space X

-- Interval [0, 1]
definition I : set ℝ := λ x, x ≤ 1 ∧ x ≥ 0
#check I

variable E : topological_space ℝ

-- Define inclusion map
definition i (x: I) : ℝ  := x

-- Define subspace topology [for Euclidean subspace topology?]
def S : topological_space I :=
topological_space.induced  i E

-- PATH
variable f : I → X

def path_topological2  {x : X} {y : X} (t : I) : X  × (I → X) ×  Prop :=
λ t, ( f t ) × f × (continuous f ∧ f 0 = x ∧ f 1 = y)

/-   type mismatch at application
prod (f t)
term
f t
has type
X : Type u_1
but is expected to have type
Type ? : Type (?+1)  -/


#### Luca Gerolla (Jul 05 2018 at 19:35):

What would be the best way to define a path? Also avoiding the type mismatch that arises in the definition?

#### Patrick Massot (Jul 05 2018 at 19:49):

I don't understand what you are trying to do. But you could have a look at data/sets/intervals in mathlib

#### Patrick Massot (Jul 05 2018 at 19:49):

But actually it may be better to have path as a structure bundling a map from reals to X and the condition that it is continuous on [0, 1].

#### Luca Gerolla (Jul 05 2018 at 20:20):

But actually it may be better to have path as a structure bundling a map from reals to X and the condition that it is continuous on [0, 1].

I was not too sure whether use create as a structure or create a definition (later I would like define homotopy; so I was thinking that (ideally) my definition of path would allow me to retrieve starting/ending points and the actual path (function f : I --> X): this for possible re-parameterisations ( I --> I ) )

I know very little about structure, but I may try to look into your suggestion. Many Thanks!

#### Luca Gerolla (Jul 05 2018 at 20:24):

I don't understand what you are trying to do. But you could have a look at data/sets/intervals in mathlib

PS: Are you referring to the part before the definition or the definition itself?
I included the code before definition just to provide more information on the interval I (and the induced subspace topology - which is meant to be induced from Euclidean topology on R ) and the topological space X of interest.

#### Johan Commelin (Jul 06 2018 at 06:43):

A path is just a continuous function I \to X, right? Or do you want a Type for paths from x to y?

#### Patrick Massot (Jul 06 2018 at 07:18):

It looks like he wants the end points to be parameters of the type

#### Kevin Buzzard (Jul 06 2018 at 07:47):

Hey Luca. So just to comment that set ℝ is a type so I is "only" a term. So when you make topological_space I something magic is happening: the term is being somehow promoted to a type. What's happening is that the term  {x : ℝ | x ≤ 1 ∧ x ≥ 0}(which is really a function) is being interpreted as the type {x : ℝ // x ≤ 1 ∧ x ≥ 0} implicitly (and this is a so-called subtype). So when you write t : I then t might not be what you think it is -- it's a term of the subtype, so it has a value t.val which is the real number, and then a proof too, called t.property.

The type mismatch is because \times, the little cross, is for making types, not terms; a term of type α × β looks like (a,b), like in maths.

#### Luca Gerolla (Jul 06 2018 at 07:47):

A path is just a continuous function I \to X, right? Or do you want a Type for paths from x to y?

Indeed, I would like the second one (a Type for paths from x to y) :)

#### Kevin Buzzard (Jul 06 2018 at 07:49):

So you could build the type using a structure. You would have to decide whether to put things like X and x and y inside the structure or outside; this is the sort of question that I am terrible at.

#### Kevin Buzzard (Jul 06 2018 at 07:52):

So it could look like

structure paths (X : Type) [topological_space X] (x y : X) :=
(f : I \to X)...


or

structure paths (X : Type) [topological_space X] :=
(start_point : X)
(end_point : X)
(f : I \to X)...


or

structure paths :=
(X : Type)
(HX : topological_space X)
(start_point : X)
...


#### Mario Carneiro (Jul 06 2018 at 07:52):

In this case you definitely want x and y outside the structure

Why?

#### Mario Carneiro (Jul 06 2018 at 07:53):

a Type for paths from x to y

:-)

#### Luca Gerolla (Jul 06 2018 at 07:53):

Hey Luca. So just to comment that set ℝ is a type so I is "only" a term. So when you make topological_space I something magic is happening: the term is being somehow promoted to a type. What's happening is that the term  {x : ℝ | x ≤ 1 ∧ x ≥ 0}(which is really a function) is being interpreted as the type {x : ℝ // x ≤ 1 ∧ x ≥ 0} implicitly (and this is a so-called subtype). So when you write t : I then t might not be what you think it is -- it's a term of the subtype, so it has a value t.val which is the real number, and then a proof too, called t.property.

The type mismatch is because \times, the little cross, is for making types, not terms; a term of type α × β looks like (a,b), like in maths.

Thank you! I am in the process of digesting this... I will try with the structure :)

#### Kevin Buzzard (Jul 06 2018 at 07:53):

and Mario is saying that you want the first of my three options above.

#### Kevin Buzzard (Jul 06 2018 at 07:54):

I suspect that you might want to make I, the unit interval, into a subtype. If you don't then you'll have coercions everywhere. You'd perhaps be better off having the coercion from I to the reals.

#### Patrick Massot (Jul 06 2018 at 07:57):

There is also the option of having the path "defined" on R but only use its values and continuity on I

#### Patrick Massot (Jul 06 2018 at 07:57):

Minimal version would be:

import analysis.real

open filter

variables {X : Type*} [topological_space X] (x y : X)

structure path :=
(map : ℝ → X)
(start_pt : map 0 = x)
(end_pt : map 1 = y)
(cont : ∀ t : ℝ, 0 ≤ t → t ≤ 1 → tendsto map (nhds t) (nhds (map t)))

instance : has_coe_to_fun (path x y) :=
⟨_, λ p, p.map⟩

example (f : path x y) : f 1 = y :=
f.end_pt


#### Mario Carneiro (Jul 06 2018 at 08:04):

Here's my suggestion:

def I01 := {x : ℝ // 0 ≤ x ∧ x ≤ 1}

instance : topological_space I01 := by unfold I01; apply_instance
instance : has_zero I01 := ⟨⟨0, le_refl _, zero_le_one⟩⟩
instance : has_one I01 := ⟨⟨1, zero_le_one, le_refl _⟩⟩

structure path {α} [topological_space α] (x y : α) :=
(to_fun : I01 → α)
(at_zero : to_fun 0 = x)
(at_one : to_fun 1 = y)
(cont : continuous to_fun)

instance {α} [topological_space α] (x y : α) : has_coe_to_fun (path x y) := ⟨_, path.to_fun⟩


#### Kevin Buzzard (Jul 06 2018 at 08:05):

@Luca Gerolla Patrick's suggestion is an interesting one. It's a very "non-maths" way to think about things, but sometimes in computer science this seems to be the way it's done. Note that cont is an explicit proof that the map is continuous (using things called filters, which is a trick to enable you to talk about things tending to other things even when there's no metric). Note also that there's a trick with variables here -- this really says structure path {X : Type} [topological_space X] (x y : X) :=... Note also that there is a problem with equality here -- you can have two different terms of type path x y which are not literally equal but which are "the same path" because the maps are different but agree on $[0,1]$.

#### Mario Carneiro (Jul 06 2018 at 08:05):

I think that in this case it is best to build up the theory of the interval as a type in its own right rather than totalizing a la isabelle

#### Patrick Massot (Jul 06 2018 at 08:06):

Note again that mathlib does have a rudimentary theory of intervals (in totally ordered types).

#### Mario Carneiro (Jul 06 2018 at 08:06):

Indeed you can prove that I01 is compact in one line

#### Patrick Massot (Jul 06 2018 at 08:07):

I'm not saying my way is best, I only wanted to point it out because, as pointed out by Kevin, it's very unlikely a mathematician or math student beginning Lean would think of it

#### Kevin Buzzard (Jul 06 2018 at 08:07):

Mario's version makes the interval a subtype, not a subset (so I01 is a type), and the tricks beforehand with the instances make it a topological space and make it so you can talk about 0 and 1. His equality is equality of paths, however you are, I assume, not going to be interested in equality anyway, but homotopy equivalence, so you'll end up putting an equivalence relation on this structure anyway.

#### Patrick Massot (Jul 06 2018 at 08:07):

The downside of Mario's version is it will be annoying to refer to any point in the interval, as seen in his definition of 0 and 1

#### Mario Carneiro (Jul 06 2018 at 08:08):

The solution to this is to define appropriate functions on I01 so that you abstract away the proof stuff

#### Mario Carneiro (Jul 06 2018 at 08:09):

For example you can probably get away with just a has_mul instance (the usual one) and a has_neg instance (the 1-x function)

#### Patrick Massot (Jul 06 2018 at 08:09):

If you are going for homotopy theory, there is a clear test case: prove that concatenation of homotopy classes of path is associative, using various modelisation choices.

#### Mario Carneiro (Jul 06 2018 at 08:10):

Also 1/2 should be a point in [0,1]

exactly

#### Mario Carneiro (Jul 06 2018 at 08:10):

from those I think you have enough to define everything else in homotopy theory

#### Kevin Buzzard (Jul 06 2018 at 08:12):

Luca -- as far as I know nobody has done this sort of stuff in Lean, however it definitely looks possible to me and hopefully not too hard. I have to do admin today so I won't be hanging around in the computer room, but I will be in the department and will pop in occasionally. I think trying to define homotopy classes of paths etc would be a fabulous exercise for you or you/Rohan.

#### Patrick Massot (Jul 06 2018 at 08:13):

It's not quite true: Johan tried it

#### Patrick Massot (Jul 06 2018 at 08:14):

https://github.com/leanprover/mathlib/pull/144

#### Patrick Massot (Jul 06 2018 at 08:14):

this has some intersection with what Luca wants to try

#### Kevin Buzzard (Jul 06 2018 at 08:14):

Oh! Luca -- this is Johan Commelin. You might want to look at what he did (or you might want to figure it out yourself)

Thanks Patrick.

#### Patrick Massot (Jul 06 2018 at 08:14):

but it's geared towards homology, and biased towards abstraction (simplicial sets everywhere)

#### Luca Gerolla (Jul 06 2018 at 08:18):

This is all very interesting, thank you very much everyone! :-)

#### Luca Gerolla (Jul 21 2018 at 11:41):

Hello, I am trying to define a function ( f  : X --> Y , where X and Y are topological spaces) in terms of its restrictions; to then exploit the fact later that if the restrictions of  f  (in this case fa : A --> Y, fb : B ---> Y - where A, B are closed , and they cover X) are continuous then the overall function  f is continuous (theorem already proved by @Kevin Buzzard ).
Unfortunately I am struggling with set.inter and the coercions that "naturally" arise; in particular when I try to give a definition for the restrictions to match  fun_match  (i.e. fa = fb on  A \and B ) and to define f as fa on A and fb on B fun_pasting_closed .

#### Luca Gerolla (Jul 21 2018 at 11:42):

This is my code:

--- Attempt to define function (f : α → β ) in terms of its restriction
variables {X Y : Type} [topological_space X]
[topological_space Y]
variable f : X → Y
variables ( A : set X ) ( B : set X)
variables (ga : A → Y ) ( gb : B → Y )

definition restriction {X Y : Type} (f : X → Y) (A : set X) : A → Y :=
λ a, f a.val

def fun_match {X Y : Type} [topological_space X]
[topological_space Y] {A B : set X} [topological_space A] [topological_space B] ( fa : A → Y ) ( fb : B → Y ) : Prop :=
sorry
--∀ x ∈  set.inter A B, fa x = fb x
--∀ x ∈ set.inter A B, fa x.val = fb x.val
--restriction fa ( set.inter A B) == restriction fb ( set.inter A B)
-- ∀ x, (restriction fa ( set.inter A B) ) x = (restriction fb ( set.inter A B) ) x

def fun_match2 {A B : set X} [topological_space A] [topological_space B] {fa : A → Y} { fb : B → Y}
( Ha : fa = restriction f A ) ( Hb : fb = restriction f B ) : Prop :=
sorry

def fun_pasting_closed {X Y : Type} [topological_space X]
[topological_space Y] {A B : set X} ( fa : A → Y ) ( fb : B → Y) { HAcont : continuous fa} { HBcont : continuous fb}
{Hunion : A ∪ B = set.univ} {HAclosed : is_closed A} {HBclosed : is_closed B}
{Hmatch : fun_match fa fb } : X → Y := sorry
--- λ t : X, if H : t ∈ A  then fa t else fb t


#### Mario Carneiro (Jul 21 2018 at 11:45):

there are way too many topological space arguments in fun_match

#### Luca Gerolla (Jul 21 2018 at 11:45):

Any help would be greatly appreciated

#### Mario Carneiro (Jul 21 2018 at 11:46):

def fun_match {X Y} {A B : set X} (fa : A → Y) (fb : B → Y) : Prop :=
∀ x h₁ h₂, fa ⟨x, h₁⟩ = fb ⟨x, h₂⟩


#### Mario Carneiro (Jul 21 2018 at 11:51):

local attribute [instance] classical.prop_decidable

noncomputable def paste {X Y} {A B : set X} (Hunion : A ∪ B = set.univ) (fa : A → Y) (fb : B → Y) (t : X) : Y :=
if h₁ : t ∈ A then fa ⟨t, h₁⟩ else
have t ∈ A ∪ B, from set.eq_univ_iff_forall.1 Hunion t,
have h₂ : t ∈ B, from this.resolve_left h₁,
fb ⟨t, h₂⟩


#### Mario Carneiro (Jul 21 2018 at 11:51):

we don't really need topology to define these functions; it only comes in for the continuity proof

#### Mario Carneiro (Jul 21 2018 at 11:56):

Here's how you can prove it has the right values:

theorem paste_left {X Y} {A B : set X} (Hunion : A ∪ B = set.univ)
(fa : A → Y) (fb : B → Y) (t : X) (h : t ∈ A) :
paste Hunion fa fb t = fa ⟨t, h⟩ :=
dif_pos _

theorem paste_right {X Y} {A B : set X} (Hunion : A ∪ B = set.univ)
(fa : A → Y) (fb : B → Y) (H : fun_match fa fb)
(t : X) (h : t ∈ B) :
paste Hunion fa fb t = fb ⟨t, h⟩ :=
by by_cases h' : t ∈ A; simp [paste, h']; apply H


#### Kenny Lau (Jul 21 2018 at 11:56):

do we really want to use the name fun_match? It is really similar to the internally generated variable _fun_match

that's fair

#### Mario Carneiro (Jul 21 2018 at 11:57):

mathlib uses eq_on for something very similar

#### Luca Gerolla (Jul 23 2018 at 10:42):

Thank you very much @Mario Carneiro
For the time being I renamed  fun_match  to  match_of_fun .
With your code the theorem  cont_of_paste  followed easily using (part of ) the pasting lemma; however, since this was done in terms of  restriction _ _ , do you see an easy way to prove that the pasted  fa , fb  are indeed  restriction f A ,  restriction f B respectively?

lemma rest_of_paste {X : Type* } {Y : Type*} {A B : set X} {Hunion : A ∪ B = set.univ} (fa : A → Y) (fb : B → Y)
{ f : X → Y } ( Hf : f = paste Hunion fa fb ) :
fa = restriction f A ∧ fb = restriction f B :=
begin split,

sorry,

sorry
end

-- prove continuity when pasted continuous restrictions on closed sets
theorem cont_of_paste {X : Type* } {Y : Type*} [topological_space X] [topological_space Y]
{ A B : set X } { Hunion : A ∪ B = set.univ} {fa : A → Y } { fb : B → Y }
{HAclosed : is_closed A} {HBclosed : is_closed B}  { Hmatch : match_of_fun fa fb }
{ f : X → Y } ( Hf : f = paste Hunion fa fb ) :
continuous fa → continuous fb → continuous f :=
begin
intros Ca Cb,
have ResA : fa = (restriction f A) , exact (rest_of_paste fa fb Hf ).1,
have ResB : fb = (restriction f B), exact (rest_of_paste fa fb Hf ).2,
rw ResA at Ca, rw ResB at Cb,
exact continuous_closed_union f Hunion HAclosed HBclosed Ca Cb
end


#### Luca Gerolla (Jul 23 2018 at 10:50):

PS: has  cont_of_paste  the right arguments? Is

{ f : X → Y } ( Hf : f = paste Hunion fa fb )


the best way to specify  f  as a paste? Asking this because I have employed a similiar method to specify arguments which were functions of certain properties/definitions, and don't know if this makes things unnecessarily more convoluted.

#### Kevin Buzzard (Jul 23 2018 at 19:53):

If you want to prove two functions are equal, the funext tactic reduces you to checking their values are equal on every input. This might be what you need?

#### Nicholas Scheel (Jul 24 2018 at 00:32):

@Luca Gerolla what about removing those two arguments and substituting f in directly? so your result would be continuous (paste Hunion fa fb)

#### Luca Gerolla (Jul 24 2018 at 09:09):

If you want to prove two functions are equal, the funext tactic reduces you to checking their values are equal on every input. This might be what you need?

 funext  does help, together with rw  and  unfold  leads to much more progress. Here is my "nearly completed" proof:

lemma rest_of_paste {X : Type* } {Y : Type*} {A B : set X} {Hunion : A ∪ B = set.univ} (fa : A → Y) (fb : B → Y)
{ f : X → Y } ( Hf : f = paste Hunion fa fb ) :
fa = restriction f A ∧ fb = restriction f B :=
begin split,
funext, unfold restriction, rw Hf, unfold paste, rw dif_pos, -- exact subtype.rec fa, exact subtype.rec_on,
have H :  x.val = (⟨ x.val, _ ⟩ : A ).val ,  trivial,
have H1 : x = ⟨x.val, _ ⟩,  exact subtype.eq ( H ), exact x.2, --rw H1,
sorry,  exact x.2,
sorry
end


Is there a way to prove  fa x = fa ⟨x.val, ?m_1⟩ ? (I thought the haves should do the job but then rw H1 fails )

#### Chris Hughes (Jul 24 2018 at 09:13):

have you tried simp or rw subtype.eta x.1 x.2

#### Mario Carneiro (Jul 24 2018 at 09:13):

cases x will make this a lot easier

#### Luca Gerolla (Jul 24 2018 at 09:14):

Yes, simp does work! Thank you Chris, very silly of me not trying it.. sorry!

#### Luca Gerolla (Jul 24 2018 at 09:42):

lemma rest_of_paste {X : Type* } {Y : Type*} {A B : set X} {Hunion : A ∪ B = set.univ} (fa : A → Y) (fb : B → Y)
{ f : X → Y } (H : match_of_fun fa fb) ( Hf : f = paste Hunion fa fb )  :
fa = restriction f A ∧ fb = restriction f B :=
begin split,
funext, unfold restriction, rw Hf,
apply eq.symm _, simp [paste_left Hunion fa fb x.val x.2],
funext, unfold restriction, rw Hf,
apply eq.symm _, simp [paste_right Hunion fa fb H x.val x.2],
end


Needed also the H hypotheses to complete the proof for fb , then paste_** simplified the proof further :)

#### Luca Gerolla (Jul 24 2018 at 09:43):

@Nicholas Scheel do you mean to rewrite the statement as

theorem cont_of_paste {X : Type* } {Y : Type*} [topological_space X] [topological_space Y]
{ A B : set X } { Hunion : A ∪ B = set.univ} {fa : A → Y } { fb : B → Y }
{HAclosed : is_closed A} {HBclosed : is_closed B}  { Hmatch : match_of_fun fa fb }
( CA : continuous fa ) ( CB : continuous fb)  : continuous (paste Hunion fa fb) := ...


?

#### Kevin Buzzard (Jul 24 2018 at 11:07):

Is there a way to prove  fa x = fa ⟨x.val, ?m_1⟩ ? (I thought the haves should do the job but then rw H1 fails )

Luca I mentioned this in my talk yesterday. The problem here is that x is \<x.val,x.property\> but you're trying to compare x with \<x.val,h\> for h some (un-named, that's why it says ?m_1) other proof of the thing that x.property is a proof of. Because these are both proofs of the same thing, they're definitionally equal by definition, so actually x = ⟨x.val, ?m_1⟩ . Take a look at theorems like subtype.eq and subtype.eta to see the various tricks that can be used, but remember that simp will know all the important ones.

#### Mario Carneiro (Jul 24 2018 at 11:07):

the easy proof is cases x, refl

#### Mario Carneiro (Jul 24 2018 at 11:08):

I usually do cases on a variable like this before proofs, because everything becomes definitionally true that way

#### Nicholas Scheel (Jul 24 2018 at 16:07):

@Luca Gerolla yes that’s what I meant, but it‘s not a big deal either way – looks like you’re making progress on it already :)

#### Kevin Buzzard (Jul 25 2018 at 00:00):

So I am a bit confused as to why typeclass inference doesn't put a topology on the subtype of a topological space. Here's some non-pasteable code:

#### Kevin Buzzard (Jul 25 2018 at 00:00):

#check Spv.is_continuous -- Spv.is_continuous : Spv ?M_1 → Prop

def Cont (R : Type) [comm_ring R] [topological_space R] [topological_ring R]
:= {vs : Spv R // Spv.is_continuous vs}

example (R : Type) [comm_ring R] [topological_space R] [topological_ring R] :
topological_space (Spv R) := by apply_instance -- works

--example (R : Type) [comm_ring R] [topological_space R] [topological_ring R] :
--topological_space (Cont R) := by apply_instance -- fails

instance (R : Type) [comm_ring R] [topological_space R] [topological_ring R] :
topological_space (Cont R) := subtype.topological_space


#### Kevin Buzzard (Jul 25 2018 at 00:01):

Spv R is a topological space, and type class inference knows this. I then make a subtype, and even though subtype.topological_space is marked as an instance, type class inference doesn't seem to work. Is this to do with topological_space being a structure with the class attribute rather than a class?

#### Kevin Buzzard (Jul 25 2018 at 00:02):

import analysis.topology.topological_space

example (X : Type) [topological_space X] (p : X → Prop) :
topological_space {x : X // p x} := by apply_instance


My MWE works :-/

#### Chris Hughes (Jul 25 2018 at 00:08):

It can infer a topological space structure on {vs : Spv R // Spv.is_continuous vs} but not if you give it a different names.

#### Chris Hughes (Jul 25 2018 at 00:08):

because type class inference looks at the expr

#### Kevin Buzzard (Jul 25 2018 at 00:09):

So am I OK to make the instance like I did?

#### Kevin Buzzard (Jul 25 2018 at 00:09):

I don't want to make diamonds

#### Chris Hughes (Jul 25 2018 at 00:10):

Don't see why not. It's a defeq diamond, and it's not even a diamond really because there's only one path it will choose.

Thanks Chris.

#### Mario Carneiro (Jul 25 2018 at 07:33):

You will notice the pattern by unfold foo; apply_instance used for this sort of situation (although an alternative is to do the first step of instance work yourself, as you did)

#### Kevin Buzzard (Jul 25 2018 at 08:42):

I think I prefer your solution -- it sounds safer. I hadn't really internalised this type class inference fact though -- so it's picky about defeq like rw?

#### Mario Carneiro (Jul 25 2018 at 08:44):

yes, it only unfolds reducible definitions

#### Mario Carneiro (Jul 25 2018 at 08:45):

This is a good thing, because it means you can attach different typeclasses to defeq things, like with_top A = with_bot A

#### Mario Carneiro (Jul 25 2018 at 08:46):

So naming a def is a way of controlling what typeclasses you want to inherit

#### Johan Commelin (Jul 25 2018 at 08:46):

I guess it sometimes makes sense to make definitions reducible. What do you think about Cont? Might that be a case where reducible makes sense?

#### Mario Carneiro (Jul 25 2018 at 08:46):

I find that it is almost never a good idea to mark a definition reducible

#### Kevin Buzzard (Jul 25 2018 at 08:50):

You make it reducible and any goal with Cont in just gets unfolded and looks more unreadable. I think.

#### Johan Commelin (Jul 25 2018 at 08:51):

Yes, so let's not do that. After all, unfolding isn't very hard to do, if we need it.

#### Luca Gerolla (Jul 27 2018 at 14:20):

Hello, has it been proved anywhere that a closed interval [r, s] is indeed closed?
I am stuck proving that a subset  T r s Hrs ( closed subinterval [r,s] ) of  I01  ( unit interval [0, 1] ) is closed

-- May be needed / useful for Guillermo - Heine-Borel Thm
theorem is_closed_int { r s : ℝ } ( Hrs : r < s ) : is_closed (int_clos Hrs) :=
begin sorry end

lemma T_is_closed  { r s : ℝ } ( Hrs : r < s ): is_closed (T r s Hrs) :=
begin unfold T,
exact is_closed_iff_nhds.2
(begin intros a H , --by_contradiction,

sorry ,
end),
end

lemma T_is_closed2  { r s : ℝ } ( Hrs : r < s ): is_closed (T r s Hrs) :=
begin unfold T,
-- Write in terms of intersection with I01 (i.e. T r s Hrs =  I01 ∧  closed_int Hrs), resolving subset nesting problem
-- Prove auxilliary lemma that (closed_int Hrs) is indeed closed
-- Use is_closed_inter to prove this lemma
--have Int : {x : ↥I01 | r ≤ x.val ∧ x.val ≤ s} = set.inter univ  (closed_int Hrs) ,
sorry,
end


With the underlying definitions

def I01 := {x : ℝ | 0 ≤ x ∧ x ≤ 1}

definition T ( a b : ℝ ) ( Hab : a < b ) : set I01 :=  { x : I01 | a ≤ x.val ∧ x.val ≤ b }

def int_clos { r s : ℝ } ( Hrs : r < s ) : set ℝ := {x : ℝ  | r ≤ x ∧ x ≤ s}


#### Kenny Lau (Jul 27 2018 at 14:20):

it's even compact

#### Luca Gerolla (Jul 27 2018 at 14:20):

it's even compact

Indeed! :)

#### Kenny Lau (Jul 27 2018 at 14:21):

what I mean is it's even proved that it is compact

#### Reid Barton (Jul 27 2018 at 14:21):

Check out the stuff around ordered_topology in analysis.topology.topological_structures, such as is_closed_le

#### Luca Gerolla (Jul 27 2018 at 14:21):

Oh, haven't thought to approach it from compactness..

#### Kenny Lau (Jul 27 2018 at 14:22):

that isn't what I mean either, what I mean is that we even proved that it is compact, so I would expect it to be proved that it is closed

#### Kevin Buzzard (Jul 27 2018 at 14:34):

Luca -- what Kenny means is "the answer to your first question is almost certainly yes". Here are some things which should be in mathlib somewhere : (1) interval [r,s] as a subspace of [0,1] with subspace topology will be closed in [0,1] if it is closed in R (2) interval [r,s] is closed in R. Reid is suggesting some places in mathlib where you might well find the theorems you want.

As a rule of thumb, when you are working on "high level" stuff like this, your first instinct should be to look in the library to see what is there. I know it sometimes feels a bit daunting but you could do worse than looking at a whole bunch of those topology files and looking through them. They are often long and complex, and written by experts so the proofs are often incomprehensible. But the trick is to find such a file, then to scan over it once and try and find the definitions, and see if you can figure out what they are supposed to be (because they are kind of like notation -- they are the language the file is written in, in some sense) and then scan over it again and try and find the statements of the main theorems. Some clues as to whether a theorem is a "main theorem" -- it might be called "theorem" rather than "lemma", it might have a docstring (a comment starting with /-- ... -/ -- note two dashes not one), or it might have a long proof. DO NOT TRY TO READ ANY LONG PROOFS!. You will get depressed and it will all seem much harder. If you find that you simply cannot understand a file because e.g. the definitions are constantly using things you've not heard of, then perhaps you started too late; look at the files which are imported at the very top and try reading one of those instead. Remember also that if a file compiles perfectly then you should be able to hover over anything and see its definition, or right click on it and see it in context.

I remember finding the files where rationals and reals were defined very intimidating to read, but that was before I started picking up some of the tricks I mention above.

#### Mario Carneiro (Jul 27 2018 at 14:55):

mathlib doesn't really use theorem vs lemma distinction (or at least I don't like to make this distinction)

#### Mario Carneiro (Jul 27 2018 at 14:57):

I'm not sure it's worth focusing on "important theorems" either when reading mathlib files - you will usually be interested in easy theorems anyway. is_closed_Icc is an easy theorem

#### Luca Gerolla (Jul 27 2018 at 15:00):

Check out the stuff around ordered_topology in analysis.topology.topological_structures, such as is_closed_le

Thank you very much, is_closed_le'  and is_closed_ge' allowed me to prove [r, s] is closed without getting to use nhds and filters!

#### Luca Gerolla (Jul 27 2018 at 15:02):

is_closed_Icc ` would have made it even quicker! (should have updated my mathlib to notice it!) :)

Last updated: May 18 2021 at 08:14 UTC