Metric space question

Stream: new members

[Jason KY.]

Hi,
I have proved that the product of two metric spaces is also a metric space:

import topology.metric_space.basic

noncomputable theory

variables {X : Type*} [metric_space X]
variables {Y : Type*} [metric_space Y]

/- The metric of any two elements of a metric space is non-negative -/
theorem metric_nonneg : ∀ x y : X, 0 ≤ dist x y := λ x y,
begin
    suffices : 0 ≤ dist y x + dist x y - dist y y,
        rw [dist_self, dist_comm, sub_zero] at this,
        linarith,
    linarith [dist_triangle y x y]
end

/- The product of two metric spaces is also a metric space -/
instance : metric_space (X × Y) :=
{   dist := λ ⟨x₀, y₀⟩ ⟨x₁, y₁⟩, dist x₀ x₁ + dist y₀ y₁,
    dist_self := λ ⟨x, y⟩, show dist x x + dist y y = 0, by simp,
    eq_of_dist_eq_zero := -- Why can't I use λ ⟨x₀, y₀⟩ ⟨x₁, y₁⟩ here?
        begin
            rintros ⟨x₀, y₀⟩ ⟨x₁, y₁⟩,
            show dist x₀ x₁ + dist y₀ y₁ = 0 → (x₀, y₀) = (x₁, y₁), intro h,
            suffices : dist x₀ x₁ = 0 ∧ dist y₀ y₁ = 0,
                rwa [eq_of_dist_eq_zero this.left, eq_of_dist_eq_zero this.right],
            split,
            all_goals {linarith [metric_nonneg x₀ x₁, metric_nonneg y₀ y₁, h]}
        end,
    dist_comm := λ ⟨x₀, y₀⟩ ⟨x₁, y₁⟩,
        show dist x₀ x₁ + dist y₀ y₁ = dist x₁ x₀ + dist y₁ y₀, by simp [dist_comm],
    dist_triangle := λ ⟨x₀, y₀⟩ ⟨x₁, y₁⟩ ⟨x₂, y₂⟩,
        show dist x₀ x₂ + dist y₀ y₂ ≤ dist x₀ x₁ + dist y₀ y₁ + (dist x₁ x₂ + dist y₁ y₂),
        by linarith [dist_triangle x₀ x₁ x₂, dist_triangle y₀ y₁ y₂]
}

but as you can see in my proof that the product of two metric spaces is also a metric space, I wasn't able to use λ ⟨x₀, y₀⟩ ⟨x₁, y₁⟩ when proving eq_of_dist_eq_zero. Why might this be?

[Reid Barton]

What happens when you try?

[Jason KY.]

It gives me

__mlocal__fresh_2827_71439 : X × Y,
_x : dist (x₀, y₀) __mlocal__fresh_2827_71439 = 0,
_fun_match : dist (x₀, y₀) __mlocal__fresh_2827_71439 = 0 → (x₀, y₀) = __mlocal__fresh_2827_71439

when I want

x₀ : X,
y₀ : Y,
x₁ : X,
y₁ : Y

which is what rintro gives me

[Reid Barton]

Weird. I have no idea.

[Jason KY.]

I'm currently trying to define a category of metric spaces but I've gotten stuck when trying to define a mapping between two metric spaces.

import topology.metric_space.basic
import category_theory.concrete_category

open category_theory
definition Metric_space := bundled metric_space

variables {X Y : Metric_space}
variables {f : X.1 → Y.1} -- invalid universe declaration, 'u_1' shadows a local universe

As you can see, I received the error invalid universe declaration, 'u_1' shadows a local universe when trying to define a mapping. What does this mean and how can I fix this?

[Reid Barton]

I don't really know why this happens, but it's better to be explicit with universe levels (just like you would write Type u)

[Jason KY.]

How would I be explicit with universe levels in this case? Sorry I don't normally use universes :/

[Reid Barton]

probably something like (untested)

import topology.metric_space.basic
import category_theory.concrete_category

universe u

open category_theory
definition Metric_space := bundled metric_space.{u}

variables {X Y : Metric_space.{u}}
variables {f : X.1 → Y.1}

[Jason KY.]

Ah! That works perfectly! Thanks

[Jason KY.]

Hi again!
I'm currently proving that the finite union of bounded sets is also bounded

/- The union of finitely many bounded subsets is also bounded -/
theorem bounded_union (S : ℕ → set X) (h₀ : ∀ n : ℕ, is_bounded $ S n) :
∀ n : ℕ, is_bounded $ ⋃ i ∈ finset.range n, S i
| 0 := by simp; constructor; refl
| (n + 1) := by simp [bounded_union_two, bounded_union]

And I'm receiving this error

failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r ℕ (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof)
Possible solutions:
  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
failed

I don't really understand what the possible solutions mean, any help would be appreciated!

[Kenny Lau]

if you include bounded_union then I suspect it will just use bounded_union on n+1

[Jason KY.]

Right, that's probably it

[Jason KY.]

Actually I'm not sure, I havebounded_union : ∀ (n : ℕ), is_bounded (⋃ (i : ℕ) (H : i ∈ finset.range n), S i) as a hypothesis. Will simp not use this instead?

[Jason KY.]

Is there a way to manually name this inductive hypothesis so it's less confusing?

[Kenny Lau]

it would be easier for me to help you if you would produce an MWE

[Jason KY.]

Alright, will do!

[Jason KY.]

This should work

import topology.metric_space.basic

variables {X : Type*} [metric_space X]

/- Notion of boundedness on metric spaces -/
def is_bounded (S : set X) := S = ∅ ∨ ∃ x₀ ∈ S, ∃ k : ℝ, ∀ x ∈ S, dist x x₀ ≤ k

/- The union of two bounded subsets is also bounded -/
lemma bounded_union_two (S T : set X) (hs : is_bounded S) (ht : is_bounded T) :
is_bounded $ S ∪ T := sorry

/- The union of finitely many bounded subsets is also bounded -/
theorem bounded_union (S : ℕ → set X) (h₀ : ∀ n : ℕ, is_bounded $ S n) :
∀ n : ℕ, is_bounded $ ⋃ i ∈ finset.range n, S i
| 0 := by simp; constructor; refl
| (n + 1) := by simp [bounded_union_two, bounded_union]

[Kenny Lau]

I don't think ⋃ i ∈ finset.range n is idiomatic

[Reid Barton]

Since n is an explicit argument, does it help if you just put bounded_union n in simp?

[Jason KY.]

Kenny Lau said:

I don't think ⋃ i ∈ finset.range n is idiomatic

Sorry but what does idiomatic mean?

[Jason KY.]

Reid Barton said:

Since n is an explicit argument, does it help if you just put bounded_union n in simp?

Emm, then simp doesn't solve the goal, but maybe it's working as intended then?

[Kenny Lau]

import topology.metric_space.basic

variables {X : Type*} [metric_space X]

/- Notion of boundedness on metric spaces -/
def is_bounded (S : set X) := S = ∅ ∨ ∃ x₀ ∈ S, ∃ k : ℝ, ∀ x ∈ S, dist x x₀ ≤ k

/- The union of two bounded subsets is also bounded -/
lemma bounded_union_two (S T : set X) (hs : is_bounded S) (ht : is_bounded T) :
is_bounded $ S ∪ T := sorry

/- The union of finitely many bounded subsets is also bounded -/
theorem bounded_union (S : ℕ → set X) (h₀ : ∀ n : ℕ, is_bounded $ S n) :
∀ n : ℕ, is_bounded $ finset.sup (finset.range n) S
| 0 := by left; simp; refl
| (n + 1) := by simpa [finset.range_succ] using bounded_union_two _ _ (h₀ _) (bounded_union n)

[Reid Barton]

Jason KY. said:

Kenny Lau said:

I don't think ⋃ i ∈ finset.range n is idiomatic

Sorry but what does idiomatic mean?

The normal way to write something. Consider ⋃ i < n.

[Kenny Lau]

Jason KY. said:

Kenny Lau said:

I don't think ⋃ i ∈ finset.range n is idiomatic

Sorry but what does idiomatic mean?

idiomatic means the same in English as in here: how people would say it

[Jason KY.]

Ah, alright!

[Kenny Lau]

Reid Barton said:

Jason KY. said:

Kenny Lau said:

I don't think ⋃ i ∈ finset.range n is idiomatic

Sorry but what does idiomatic mean?

The normal way to write something. Consider ⋃ i < n.

I... don't think that's idiomatic either

[Kenny Lau]

because there's not enough lemmas to reduce from n+1 to n

[Jason KY.]

Right, I'll try to use finset.sup in the future then, thanks for the help!

[Kenny Lau]

I don't know what's idiomatic actually. When do we use a finite union?

[Kenny Lau]

I mean, this lemma has nothing to do with is_bounded: it's just induction from bounded_union_two

[Reid Barton]

ok yes

[Reid Barton]

lemma set.finite.compact_bUnion {s : set β} {f : β → set α} (hs : finite s)
  (hf : ∀i ∈ s, compact (f i)) :
  compact (⋃i ∈ s, f i) :=

[Reid Barton]

lemma compact_Union {f : β → set α} [fintype β]
  (h : ∀i, compact (f i)) : compact (⋃i, f i) :=

[Kenny Lau]

huh

[Reid Barton]

I didn't really pay attention to the whole statement of Jason's lemma.

[Jason KY.]

Emm, I'm a bit confused. When should we use what?

[Jason KY.]

I was able to get it working by introducing a temp lemma

lemma temp (S : ℕ → set X) (n : ℕ) : (⋃ i ∈ finset.range (n + 1), S i) = (⋃ i ∈ finset.range n, S i) ∪ S (n + 1)
:= sorry

/- The union of finitely many bounded subsets is also bounded -/
theorem bounded_union (S : ℕ → set X) (h₀ : ∀ n : ℕ, is_bounded $ S n) :
∀ n : ℕ, is_bounded $ ⋃ i ∈ finset.range n, S i
| 0 := by simp; constructor; refl
| (n + 1) := by simp [temp, bounded_union_two, bounded_union n, h₀ (n + 1)]

Is there something like temp in mathlib?

[Reid Barton]

I would suggest imitating the statement of set.finite.compact_bUnion and using finset.induction_on in the proof

[Reid Barton]

Your statement is not going to be very convenient to use anyways so why bother proving it?

[Reid Barton]

Unless it happens to be exactly what you need for some application

[Jason KY.]

Oh, I'm just learning metric spaces myself so I thought to prove all the theorems in my lecture notes in LEAN

[Jason KY.]

Reid Barton said:

I would suggest imitating the statement of set.finite.compact_bUnion and using finset.induction_on in the proof

Right, I'll try to do this

[Reid Barton]

Normally the finite set indexing your sets won't happen to be of the form finset.range n and then you would have to do a lot of work to massage things into a situation in which you can apply your bounded_union.

[Jason KY.]

Hi,
I would now like to define the notion of open in LEAN however I've gotten a bit stuck.

/- Definition of an open ball -/
def open_ball (x₀ : X) (r : ℝ) (h : 0 < r) := {x : X | dist x₀ x < r}

/- Definition of being open -/
def is_open' (S : set X) := ∀ s ∈ S, ∃ ε > 0, open_ball s ε H ⊆ S

As you can see, my definition of an open ball requires the radius to be positive but this makes things rather awkward as then I would need to refer to a proof that r > 0 whenever I would like to create an open ball.

/- Definition of being open -/
def is_open' (S : set X) := ∀ s ∈ S, ∃ ε : ℝ, (hε : 0 < ε), open_ball s ε hε ⊆ S

I was hoping something like this would work but unfortunately, it does not. Is there an easy way of doing this? (Or even better, perhaps a type calledℝ⁺ which is the positive reals?)

[Patrick Massot]

I think you have too many commas.

[Patrick Massot]

But I can't be sure because you didn't provide a MWE.

[Reid Barton]

∀ s ∈ S, ∃ (ε : ℝ) (hε : 0 < ε), open_ball s ε hε ⊆ S

[Reid Barton]

is at least syntactically correct

[Jason KY.]

Ah, I see! thanks!

[Patrick Massot]

But it's still a bad idea to include the positivity constraint in the definition of open_ball.

[Jason KY.]

is it? It's what my lecture notes said atleast

[Patrick Massot]

Your lecture notes don't include type theoretic convenience constraints.

[Jason KY.]

Why would it be a bad idea with these constraints?

[Patrick Massot]

You saw why putting this in the definition of balls is a bad idea.

[Jason KY.]

Right... But I don't see a better solution if I would like to use the definition presented in my lecture notes so I guess I just have to deal with it :D

[Patrick Massot]

I think your lecturer wouldn't notice this difference in the definition of balls. Of course the definition of open subsets must include a positive radius condition.

[Jason KY.]

Okay, I'll try to do without this restriction and just apply the positive radius and see if I run into trouble. Thanks again!

[Patrick Massot]

I mean you can change your code to

/- Definition of an open ball -/
def open_ball (x₀ : X) (r : ℝ) := {x : X | dist x₀ x < r}

/- Definition of being open -/
def is_open' (S : set X) := ∀ s ∈ S, ∃ ε > 0, open_ball s ε ⊆ S

[Jason KY.]

I've changed it to this because I've heard you should always use < rather than >

/- Definition of being open -/
def is_open' (S : set X) := ∀ s ∈ S, ∃ (ε : ℝ) (hε : 0 < ε), open_ball s ε ⊆ S

[Jason KY.]

But I guess it doesn't really matter either way

[Patrick Massot]

I would keep the natural writing order here.

[Kevin Buzzard]

Oh! There are cases when >is OK?

[Patrick Massot]

I'm lobbying that it should be allowed precisely in this case (when appearing in a quantifier).

[Kevin Buzzard]

That's interesting because appearing in a quantifier of this form is the only time I ever miss > but I tell Xenaites to use < or else they'll get linted.

[Patrick Massot]

You can always plea the linter's indulgence.

[Patrick Massot]

with @[nolint ge_or_gt]

[Jason KY.]

Following @Reid Barton 's suggestion, I've been trying to use set.finite.induction_on but I'm not sure if the way I'm using it is correct.
Below is a MWE of my current problem:

import topology.metric_space.basic

variables {X : Type*} [metric_space X]

/- Definition of an open ball -/
def open_ball (x₀ : X) (r : ℝ) := {x : X | dist x₀ x < r}

/- Definition of being open -/
def is_open' (S : set X) := ∀ s ∈ S, ∃ (ε : ℝ) (hε : 0 < ε), open_ball s ε ⊆ S

/- The intersect of open sets is open -/
lemma inter_open_is_open (U₀ U₁ : set X)
(h₀ : is_open' U₀) (h₁ : is_open' U₁) : is_open' (U₀ ∩ U₁) := sorry

lemma inter_finite_open_is_open (I : set ℕ) (U : ℕ → set X) {hI : set.finite I}
(h₀ : ∀ i ∈ I, is_open' $ U i) : is_open' $ ⋂ i ∈ I, U i :=
set.finite.induction_on hI (λ x, by simp; from ⟨1, by norm_num⟩) $ λ i S hi hS hopen,
begin
    rw set.bInter_insert,
    apply inter_open_is_open,
        {apply h₀, sorry},
        assumption
end

I feel that after applying induction, there should be a term like is_open' (U i)but there is not. What have I done wrong here?

[Alex J. Best]

If you move h₀ into the statement you can make it work, caveat lector: I didn't think too hard about the best way to do it, just followed my nose at every subgoal.

lemma inter_finite_open_is_open (I : set ℕ) (U : ℕ → set X) {hI : set.finite I}
: ( ∀ i ∈ I, is_open' $ U i) → (is_open' $ ⋂ i ∈ I, U i) :=
set.finite.induction_on hI (λ x, by simp; begin intro, intro, use 1, split, exact zero_lt_one,exact set.subset_univ (open_ball s 1), end) $ λ i S hi hS hopen,
begin
    rw set.bInter_insert,intros,
    apply inter_open_is_open,
        {apply a, exact set.mem_insert i S, },
        apply hopen,intros,
        apply a,exact set.mem_union_right (λ (a : ℕ), a = i) H,
end

[Jason KY.]

Thank you so much Alex!

[Jason KY.]

I'll try to put such predicates in the statement in the future. Don't think it would hurt right?

[Alex J. Best]

Well normally its annoying to have to explicitly intro them and name them at the start of the proof, but for induction type proofs, its sometimes needed.

[Jason KY.]

Hi!
I'm slightly stuck on trying to manipulate the following intersect

import topology.metric_space.basic

variables {X : Type*} [metric_space X]

/- Definition of an open ball -/
def open_ball (x₀ : X) (r : ℝ) := {x : X | dist x₀ x < r}

/- Definition of being open -/
def is_open' (S : set X) := ∀ s ∈ S, ∃ (ε : ℝ) (hε : 0 < ε), open_ball s ε ⊆ S

/- Definition of being closed -/
def is_closed' (S : set X) := is_open' $ -S

/- Definition of closure -/
def closure' (S : set X) := ⋂ (T : set X) (h₀ : S ⊆ T) (h₁ : is_closed' T), T

attribute [reducible] open_ball is_open' is_closed'

lemma closure_closed (S : set X) : is_closed' $ closure' S :=
begin
    unfold closure', -- ⊢ is_closed' (⋂ (T : set X) (h₀ : S ⊆ T) (h₁ : is_closed' T), T)
    sorry
end

I would like to use a lemma I've proved which it that the intersect of closed sets is closed :

theorem Inter_closed_is_closed (I : set Type*) (U : Type* → set X)
(h : ∀ i ∈ I, is_closed' $ U i) : is_closed' $ ⋂ i ∈ I, U i := sorry

How should I go about doing this?

[Reid Barton]

The statement of your lemma is not good. Compare is_open_bUnion.

[Jason KY.]

Is the statement bad because of the squiggly brackets or because of the Type*s?

[Reid Barton]

The Type*s

[Reid Barton]

You should replace those with an arbitrary type

[Jason KY.]

Like this?

theorem Inter_closed_is_closed (I : set Type) (U : Type → set X)
(h : ∀ i ∈ I, is_closed' $ U i) : is_closed' $ ⋂ i ∈ I, U i := sorry

[Reid Barton]

No, what is set Type for? I think you are confusing Type with the concept of "some type". Study what happens near the start of topology.basic.

[Jason KY.]

Ah, I see. So it should be like this?

variable {α : Type*}
theorem Inter_closed_is_closed {I : set α} {U : α → set X}
(h : ∀ i ∈ I, is_closed' $ U i) : is_closed' $ ⋂ i ∈ I, U i := sorry

[Reid Barton]

Yes. you might find you need additional lemmas though, I'm not sure.

[Jason KY.]

I think it works, let me try to finish the proof

[Jason KY.]

I couldn't get it working :/ But if I change the definition of my closure then it works:

/- Definition of closure -/
def closure'' (S : set X) := ⋂ (T : set X) (h₀ : S ⊆ T ∧ is_closed' T), T

/- The closure of a set is also closed -/
lemma closure_closed (S : set X) : is_closed' $ closure'' S :=
Inter_closed_is_closed $
begin
    intros T hT,
    from hT.right
end

It there a way to change ⋂ (T : set X) (h₀ : S ⊆ T) (h₁ : is_closed' T), T to ⋂ (T : set X) (h₀ : S ⊆ T ∧ is_closed' T), T.
They are the same right?

[Mario Carneiro]

did you try simp?

[Mario Carneiro]

that's the sort of thing that simp is likely to know

[Jason KY.]

Just tried it, doesn't work :/

[Mario Carneiro]

The lemma you need is infi_and, not sure if that has a set version but it's defeq to it

[Jason KY.]

Alright, I'll try it out!

[Mario Carneiro]

You should prove the version without the set, because it is more general

theorem Inter_closed_is_closed {α} {U : α → set X}
  (h : ∀ i, is_closed' $ U i) : is_closed' $ ⋂ i, U i := sorry

variable {α : Type*}
theorem bInter_closed_is_closed {I : set α} {U : α → set X}
  (h : ∀ i ∈ I, is_closed' $ U i) : is_closed' $ ⋂ i ∈ I, U i :=
Inter_closed_is_closed $ λ i, Inter_closed_is_closed $ λ h', h i h'

[Mario Carneiro]

def closure' (S : set X) := ⋂ (T : set X) (h₀ : S ⊆ T) (h₁ : is_closed' T), T

/- The closure of a set is also closed -/
lemma closure_closed (S : set X) : is_closed' $ closure' S :=
Inter_closed_is_closed $ λ T, Inter_closed_is_closed $ λ h₁,
Inter_closed_is_closed $ λ h₂, h₂

[Mario Carneiro]

Note that Inter_closed_is_closed has its own version of {α}, which is actually {α : Sort*}, so that it can also apply when the index type is a prop

[Mario Carneiro]

if you reuse the variable it will be {α : Type*} which doesn't apply to Prop

[Jason KY.]

So {α} is just short for {α : Sort*}?

[Mario Carneiro]

Yes. Note that Sort* is actually Sort _, a metavariable that will be instantiated depending on the rest of the statement. So for example if you use this in the second statement:

theorem bInter_closed_is_closed {α} {I : set α} {U : α → set X}
  (h : ∀ i ∈ I, is_closed' $ U i) : is_closed' $ ⋂ i ∈ I, U i := ...

then {α} will get type {α : Type u_1} because that's what is needed to make set α typecheck

[Jason KY.]

Ah, I see. Thank you!