## Stream: new members

### Topic: Why uniform_space?

#### Damiano Testa (Dec 09 2020 at 20:13):

Dear All,

I am trying to prove the lemma below. I thought that is_open_ball was all I needed, but I seem to have to use that a metric_space is a uniform_space.

Does anyone know how I can finish the proof?

Thanks!

import topology.metric_space.basic

open topological_space metric

example {α : Type*} [topological_space α] [metric_space α] (x y : α) (yc : y ∈ ({x} : set α)ᶜ) :
is_open (ball y (dist y x)) :=
begin
convert @is_open_ball α _inst_2 y (dist y x),
sorry,
end


#### Kevin Buzzard (Dec 09 2020 at 20:14):

Just checking -- is that really the way to set up the example? It might say "alpha is a topological space and a metric space, but these two structures are entirely unrelated"

Ah, let me try!

#### Damiano Testa (Dec 09 2020 at 20:15):

Sorry, you are perfectly right!

Thanks!

#### Kevin Buzzard (Dec 09 2020 at 20:15):

yeah, your way is a lot harder :-)

#### Damiano Testa (Dec 09 2020 at 20:16):

Indeed, I struggled for a little bit, not realizing what was going on!

#### Damiano Testa (Dec 09 2020 at 20:18):

Given that we are here. Is there a t1_space instance on metric_space? (Or indeed, most of the t_i_space instances?)

there should be

#### Damiano Testa (Dec 09 2020 at 20:19):

(This is where the question came from: I defined a t1_space instance, thinking that it would be easy, and it is if I do not use two different topological space structures! :face_palm: )

#### Kevin Buzzard (Dec 09 2020 at 20:21):

import topology.metric_space.basic

open topological_space metric

example {α : Type*} [metric_space α] : t1_space α := by apply_instance


Yes.

#### Kevin Buzzard (Dec 09 2020 at 20:21):

This had to be there, otherwise Patrick's proof the other day wouldn't have worked.

#### Mario Carneiro (Dec 09 2020 at 20:22):

I'm trying to answer this question the hard way, by reading the sources

#### Kevin Buzzard (Dec 09 2020 at 20:22):

example {α : Type*} [metric_space α] : t1_space α := by show_term {apply_instance} is the easy way now

#### Damiano Testa (Dec 09 2020 at 20:22):

Ok, I think all my confusion started with the two separate assumption topological_space and metric_space.

Thanks for clearing this up for me!

#### Kevin Buzzard (Dec 09 2020 at 20:23):

I didn't really get typeclasses until I actually made something which used them (schemes)

#### Mario Carneiro (Dec 09 2020 at 20:25):

I see that uniform_space.basic imports topology.separation but it doesn't actually use anything in the file

write a linter!

#### Kevin Buzzard (Dec 09 2020 at 20:26):

isn't that what you kids do?

#### Mario Carneiro (Dec 09 2020 at 20:28):

Hm, we don't have that metric spaces are normal though

#### Adam Topaz (Dec 09 2020 at 20:36):

Even better:

import topology.metric_space.basic
example {X : Type*} [metric_space X] : regular_space X := by apply_instance


#### Adam Topaz (Dec 09 2020 at 20:38):

What comes after t3?

#### Mario Carneiro (Dec 09 2020 at 20:38):

regular, then normal

#### Adam Topaz (Dec 09 2020 at 20:39):

regular = t3 right?

yeah

#### Mario Carneiro (Dec 09 2020 at 20:39):

I think there is another one in between

#### Kevin Buzzard (Dec 09 2020 at 20:39):

Are regular and normal really words for topological spaces? They're also predicates on commutative rings. Regular implies normal for commutative rings

they are

#### Kevin Buzzard (Dec 09 2020 at 20:39):

maths is so messed up

#### Adam Topaz (Dec 09 2020 at 20:39):

normal implies regular for spaces :sad:

#### Kevin Buzzard (Dec 09 2020 at 20:40):

that's because spec is contravariant

#### Adam Topaz (Dec 09 2020 at 20:40):

Wikipedia says there's TX for X in {0,1,2,2.5,3,3.5,4,5,6}

#### Mario Carneiro (Dec 09 2020 at 20:41):

• X is T0, or Kolmogorov, if any two distinct points in X are topologically distinguishable. (It will be a common theme among the separation axioms to have one version of an axiom that requires T0 and one version that doesn't.)
• X is R0, or symmetric, if any two topologically distinguishable points in X are separated.
• X is T1, or accessible or Fréchet or Tikhonov, if any two distinct points in X are separated. Thus, X is T1 if and only if it is both T0 and R0. (Although you may say such things as "T1 space", "Fréchet topology", and "suppose that the topological space X is Fréchet"; avoid saying "Fréchet space" in this context, since there is another entirely different notion of Fréchet space in functional analysis.)
• X is R1, or preregular, if any two topologically distinguishable points in X are separated by neighbourhoods. Every R1 space is also R0.
• X is Hausdorff, or T2 or separated, if any two distinct points in X are separated by neighbourhoods. Thus, X is Hausdorff if and only if it is both T0 and R1. Every Hausdorff space is also T1.
• X is T2½, or Urysohn, if any two distinct points in X are separated by closed neighbourhoods. Every T2½ space is also Hausdorff.
• X is completely Hausdorff, or completely T2, if any two distinct points in X are separated by a continuous function. Every completely Hausdorff space is also T2½.
• X is regular if, given any point x and closed set F in X such that x does not belong to F, they are separated by neighbourhoods. (In fact, in a regular space, any such x and F will also be separated by closed neighbourhoods.) Every regular space is also R1.
• X is regular Hausdorff, or T3, if it is both T0 and regular.[1] Every regular Hausdorff space is also T2½.
• X is completely regular if, given any point x and closed set F in X such that x does not belong to F, they are separated by a continuous function. Every completely regular space is also regular.
• X is Tychonoff, or T3½, completely T3, or completely regular Hausdorff, if it is both T0 and completely regular.[2] Every Tychonoff space is both regular Hausdorff and completely Hausdorff.
• X is normal if any two disjoint closed subsets of X are separated by neighbourhoods. (In fact, a space is normal if and only if any two disjoint closed sets can be separated by a continuous function; this is Urysohn's lemma.)
• X is normal regular if it is both R0 and normal. Every normal regular space is regular.
• X is normal Hausdorff, or T4, if it is both T1 and normal. Every normal Hausdorff space is both Tychonoff and normal regular.
• X is completely normal if any two separated sets are separated by neighbourhoods. Every completely normal space is also normal.
• X is completely normal Hausdorff, or T5 or completely T4, if it is both completely normal and T1. Every completely normal Hausdorff space is also normal Hausdorff.
• X is perfectly normal if any two disjoint closed sets are precisely separated by a continuous function. Every perfectly normal space is also completely normal.
• X is perfectly normal Hausdorff, or T6 or perfectly T4, if it is both perfectly normal and T1. Every perfectly normal Hausdorff space is also completely normal Hausdorff.

I feel like the list gets longer every time I look at it

#### Adam Topaz (Dec 09 2020 at 20:42):

Right. Time to switch to condensed sets then.

#### Kevin Buzzard (Dec 09 2020 at 20:47):

@Damiano Testa if you're still around, then here's something you might want to think about. In #4301 there is the following proof:

lemma non_root_interval_of_polynomial (α : ℝ) (f : polynomial ℝ) (h_f_nonzero : f ≠ 0) :
∃ B : ℝ, 0 < B ∧ ∀ x (hr : abs (α - x) < B) (hn : x ≠ α), f.eval x ≠ 0 :=
begin
set f_roots := f.roots.to_finset.erase α,
set distances := insert (1 : ℝ) (f_roots.image (λ x, abs (α - x))),
have h_nonempty : distances.nonempty := ⟨1, finset.mem_insert_self _ _⟩,
set B := distances.min' h_nonempty with hB,
have h_allpos : ∀ x : ℝ, x ∈ distances → 0 < x,
{ intros x hx, rw [finset.mem_insert, finset.mem_image] at hx,
rcases hx with rfl | ⟨α₀, ⟨h, rfl⟩⟩,
{ exact zero_lt_one },
{ rw [finset.mem_erase] at h,
rw [abs_pos, sub_ne_zero], exact h.1.symm }},
use [B, (h_allpos B (distances.min'_mem h_nonempty))],
intros x hx hxα,
have hab₂ : x ∉ f.roots.to_finset,
{ intro h,
have h₁ : x ∈ f_roots, { rw [finset.mem_erase], exact ⟨hxα, h⟩ },
have h₂ : abs (α - x) ∈ distances,
{ rw [finset.mem_insert, finset.mem_image], right, exact ⟨x, ⟨h₁, rfl⟩⟩ },
have h₃ := finset.min'_le distances (abs (α - x)) h₂,
erw ←hB at h₃, linarith only [lt_of_lt_of_le hx h₃] },
rwa [multiset.mem_to_finset, mem_roots h_f_nonzero, is_root.def] at hab₂
end


(to make it run you need to go to a local copy of mathlib, checkout liouville_theoerm/lemmas, type leanproject get-cache and then open analysis/real/polynomial.lean). This PR is making the same mistake you were making earlier. Can you make that proof about 1/4 the length?

#### Mario Carneiro (Dec 09 2020 at 20:47):

Hm, so I started trying to prove this and got stuck on the very first step:

import topology.uniform_space.separation

open topological_space
open_locale classical topological_space uniformity filter

instance separated_normal {α} [uniform_space α] [separated_space α] : normal_space α :=
⟨λs t hs ht d, begin
have : {p : α × α | p.1 ∈ s → p.2 ∉ t} ∈ 𝓤 α,
{ sorry },
end⟩


why should this be true?

#### Mario Carneiro (Dec 09 2020 at 20:49):

it seems like you might need some kind of compactness property to be able to get all the neighborhoods together

ah, it's false

#### Damiano Testa (Dec 09 2020 at 20:57):

@Kevin Buzzard it was looking at liouville that I decided to prove the lemma about discreteness of roots of polynomials: I am indeed planning to apply this to make the arguments quicker! Though, tonight I should rest: assuming two topologies on the same space was my cue!

Last updated: May 13 2021 at 00:41 UTC