Trying to prove: any strict subspace has empty interior

Stream: general

[sty]

Hi, I'm an undergraduate who's fairly new at Lean, so there may be some misunderstandings not only about the way Lean works but also about math. I've read most of "Theorem Proving In Lean" ("Release 3.23.0") and am trying to wrap my head around some code in mathlib.

My current underlying goal is to write a proof of "For any given normed vector space E and any strict subspace F (i.e. any subspace that is not equal to E), the interior of F in E is empty."

I've looked at the code for normed spaces in mathlib, and tried to start things from there, specifically looking at the proof of "the interior of a closed ball is a ball" because it looks like the closest thing I could find from what I want to prove. But the whole file has bits that I don't understand. I started with this:

import analysis.normed_space.basic

variables {𝕂 : Type*} [normed_field 𝕂]
variables {E : Type*} [seminormed_add_comm_group E] [normed_space 𝕂 E]

theorem strict_subspace_empty_interior (F: submodule 𝕂 E): (interior F).isempty :=
    sorry

But "interior F" is not defined since I defined F not as a set, but as a submodule of E. From this I gather that F should have some sort of normed space structure, but I don't really understand how to use it. Also, if I replace "interior F" with "interior E", it still doesn't work as a normed space doesn't seem to have an underlying set structure in mathlib. Now I think I understand that modules and stuff like that aren't always proper sets, but a normed space should be, since the norm is a blatant function from the space to the set of real numbers. Perhaps I missed something but I believe nothing in mathlib gives a set structure to normed spaces, so I'm a bit lost here.

There will probably be more issues when I eventually try to complete the proof, but that's where I'm at currently. Please feel free to suggest any resources that I may have overlooked.

[Johan Commelin]

What happens if you write interior (F : set E) instead of interior F?

[Johan Commelin]

Note that you are missing the assumption that F is proper. You can add (hF : F ≠ ⊤) to do that.

[Johan Commelin]

⊤ = \top is the "top element".

[Johan Commelin]

sty said:

... doesn't seem to have an underlying set structure in mathlib. Now I think I understand that modules and stuff like that aren't always proper sets, but a normed space should be, since the norm is a blatant function from the space to the set of real numbers. Perhaps I missed something but I believe nothing in mathlib gives a set structure to normed spaces, so I'm a bit lost here.

There will probably be more issues when I eventually try to complete the proof, but that's where I'm at currently. Please feel free to suggest any resources that I may have overlooked.

Talking about a "set structure" doesn't have a precise meaning in Lean. But for all practical purpose these things are "sets" in the colloquial mathematical meaning of the word.
However, interior is only defined for terms of type set X, where X is topological space (strictly, a Type + instance of topological_space). Now this is maybe linguistically confusing, but set X means "set of terms of type X". In other words, set X is the "powerset" aka "subsets of X".

[Johan Commelin]

But F is a submodule of E, so Lean will know how to turn it into a "subset". You can do that by writing (F : set E).

[Patrick Massot]

There is also a confusion about is_empty.

[sty]

Thank you, that helps me a lot!

Now, why is it needed to use ⊤? I think I understand why F ≠ E makes no sense (since F and E aren't the same type), but then what object does ⊤ really refer to?

Also I've just figured out now that submodule does have a carrier property that gives a set, but module doesn't seem to. Why is that?

And yes, there was a confusion about is_empty, I typed that from memory, thanks for pointing it out :D
Here's where I'm at now:

import analysis.normed_space.basic

variables {𝕂 : Type*} [normed_field 𝕂]
variables {E : Type*} [seminormed_add_comm_group E] [normed_space 𝕂 E]

theorem strict_subspace_empty_interior (F: submodule 𝕂 E): F ≠ ⊤  -> ¬(interior (F : set E)).nonempty :=
    sorry

The "is not nonempty" thing looks kind of weird to me, is there a cleaner way to write it?

[Patrick Massot]

You can write interior (F : set E) = ∅

[Johan Commelin]

In ordinary mathematics, you can't really distinguish ⊤ : submodule K E from E itself. But ⊤ is the module viewed as submodule of itself.

[Patrick Massot]

Nowadays I frequently catch myself saying things like "E seen as a submodule of itself" in lectures...

[Eric Wieser]

It's a secret ploy to lay foundations for converting your students to Lean later

[sty]

Patrick Massot said:

You can write interior (F : set E) = ∅

that does work, but then I run into this issue again (I'm starting the proof with the contrapose and assume tactics, then I think I need to apply the cases tactic in order to get an element from the (assumed) non-empty interior without using the axiom of choice, but I can't really figure out a way from ¬interior ↑F = ∅ to (interior F).nonempty)

[Johan Commelin]

Why "without using the axiom of choice"?

[Patrick Massot]

It will probably be easier to first prove the contrapositive:

theorem strict_subspace_empty_interior (F: submodule 𝕂 E) (hF : (interior (F : set E)).nonempty) :
  F = ⊤

[Patrick Massot]

Also, your statement is false, that will be an obstacle at some point (but much later).

[Patrick Massot]

By the way, are you interested in knowing that (a correct version of) this lemma is already in mathlib or are you doing an exercise anyway?

[sty]

Johan Commelin said:

Why "without using the axiom of choice"?

I'm referring to this message and the ones above it, which give a way to take an element from a non-empty set, but using that axiom.

Patrick Massot said:

It will probably be easier to first prove the contrapositive:

theorem strict_subspace_empty_interior (F: submodule 𝕂 E) (hF : (interior (F : set E)).nonempty) :
  F = ⊤

Yes, that's what I'm trying to do. The first line of my proof (right after begin) is actually contrapose,. Is that bad practice?

[sty]

Patrick Massot said:

By the way, are you interested in knowing that (a correct version of) this lemma is already in mathlib or are you doing an exercise anyway?

I am interested indeed! Please show me. (the lemma that I am trying to prove was actually given as a class exercise unrelated to Lean, but I may have lost some detail in the translation, since it was in French originally and I also may have misunderstood it)

[Patrick Massot]

The issue in your code is variables {𝕂 : Type*} [normed_field 𝕂] which isn't as strong as what you hope for.

[Mario Carneiro]

I assume it's false in the case where the topology is discrete

[Patrick Massot]

Where are you studying and in which year?

[Patrick Massot]

The lemma in mathlib is docs#submodule.eq_top_of_nonempty_interior' but you will probably have some difficulties reading it if your math background is in standard undergrad maths.

[sty]

Patrick Massot said:

Where are you studying and in which year?

Second year of CPGE MP. The exercise in French is "Soit E un EVN. Montrer que tout sous-espace vectoriel strict F de E est d'intérieur vide." (EVN stands for "espace vectoriel normé").

Mario Carneiro said:

I assume it's false in the case where the topology is discrete

Oh, then as Patrick Massot said, it's something that isn't covered at my level.

Patrick Massot said:

The lemma in mathlib is docs#submodule.eq_top_of_nonempty_interior' but you will probably have some difficulties reading it if your math background is in standard undergrad maths.

I'll try to give it a read. Thank you.

[Patrick Massot]

The key point is that "EVN" probably mean $\mathbb{R}\text{ or } \mathbb{C}$-evn in your context.

[Patrick Massot]

The issue with your statement is that the norm on $\mathbb{K}$ could be the norm sending $0_\mathbb{K}$ to $0_\mathbb{R}$ and everything else to $1_\mathbb{R}$.

[Patrick Massot]

I think that if you want to get back on track with elementary maths you can start with

import analysis.normed_space.basic

variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]

open_locale topological_space
open set filter function metric

theorem strict_subspace_empty_interior (F: submodule ℝ E) (hF : (interior (F : set E)).nonempty) :
  F = ⊤ :=
begin
  rcases hF with ⟨x, hx⟩,
  refine (submodule.eq_top_iff'.2 $ λ y, _),
  rcases nhds_basis_ball.mem_iff.mp (mem_interior_iff_mem_nhds.mp hx) with ⟨ε, ε_pos, hε⟩,
  obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > (0 : ℝ), x + δ • (y - x) ∈ ball x ε,
  {
    sorry },
end

[Patrick Massot]

The two lines that start with open at the top are very probably overkill, but I always start with those in this context. Presumably open metric is enough.

[Patrick Massot]

I fear the intermediate goal will be painful because stupid inequality arguments are painful in Lean. Maybe @Heather Macbeth will want to save you.

[Patrick Massot]

By the way, both proving this intermediate goal and using it will be much easier if you draw a picture first. Lean doesn't change anything to this basic fact of mathematics.

[Anatole Dedecker]

Let me suggest another approach, which may not be really shorter, but seems way more natural to me: first translating everything to zero, and then messing with norms.

import analysis.normed_space.basic

variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]

open_locale topological_space
open set filter function metric

theorem strict_subspace_empty_interior (F: submodule ℝ E) (hF : (interior (F : set E)).nonempty) :
  F = ⊤ :=
begin
  rcases hF with ⟨x, hx⟩,
  refine (submodule.eq_top_iff'.2 $ λ y, _),
  rcases nhds_basis_ball.mem_iff.mp (mem_interior_iff_mem_nhds.mp hx) with ⟨ε, ε_pos, hε⟩,
  have fact₁ : ball 0 ε ⊆ (F : set E),
  { sorry }, -- translation
  have fact₂ : ∃ δ > (0 : ℝ), ‖δ • y‖ < ε,
  { sorry }, -- still annoying in Lean, but mathematically trivial
  sorry
end

[Anatole Dedecker]

(deleted)

[Anatole Dedecker]

Patrick Massot said:

I think that if you want to get back on track with elementary maths you can start with

import analysis.normed_space.basic

variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]

open_locale topological_space
open set filter function metric

theorem strict_subspace_empty_interior (F: submodule ℝ E) (hF : (interior (F : set E)).nonempty) :
  F = ⊤ :=
begin
  rcases hF with ⟨x, hx⟩,
  refine (submodule.eq_top_iff'.2 $ λ y, _),
  rcases nhds_basis_ball.mem_iff.mp (mem_interior_iff_mem_nhds.mp hx) with ⟨ε, ε_pos, hε⟩,
  obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > (0 : ℝ), x + δ • (y - x) ∈ ball x ε,
  {
    sorry },
end

I'm actually surprised that the proof we have in mathlib goes along these lines, taking care of both the translation and the rescaling at once, because to me the obvious first step would be to translate everything back to zero and then star thinking :sweat_smile: