Addition of interiors

Stream: Is there code for X?

[Yaël Dillies]

I feel like this is basically the definition of has_continuous_add, but I can't pin down what to do exactly.

import topology.algebra.module

open_locale pointwise

lemma interior_add_interior_subset {α : Type*} [topological_space α] [add_comm_group α]
  [has_continuous_add α] {s t : set α} :
  interior s + interior t ⊆ interior (s + t) :=

[Yaël Dillies]

And in the same vein I also need

lemma is_open_map_neg : is_open_map (λ x : α, -x) := sorry

lemma is_open_map_add : is_open_map (λ x : α × α, x.1 + x.2) := sorry

lemma is_open_map_sub : is_open_map (λ x : α × α, x.1 - x.2) := sorry

[Heather Macbeth]

For the latter ones, check out docs#homeomorph.neg, thus you can do homeomorph.neg.is_open_map. We have homeomorph.add too, but it would only give openness of addition-with-left-variable-fixed.

[Heather Macbeth]

The first one reduces to one of your second lemmas, the openness of the full addition map.

import topology.algebra.module

open_locale pointwise

variables {α : Type*} [topological_space α] [add_comm_group α]

lemma is_open_map_add : is_open_map (λ x : α × α, x.1 + x.2) := sorry

lemma interior_add_interior_subset {s t : set α} :
  interior s + interior t ⊆ interior (s + t) :=
begin
  rw subset_interior_iff_subset_of_open,
  { rintros x ⟨a, b, ha, hb, rfl⟩,
    exact set.add_mem_add (interior_subset ha) (interior_subset hb) },
  { rw ← set.add_image_prod,
    apply is_open_map_add,
    rw is_open_prod_iff',
    left,
    exact ⟨is_open_interior, is_open_interior⟩ }
end

[Yaël Dillies]

I'mstealingthatproofthankyouverymuch

[Heather Macbeth]

Actually, slicker proof that doesn't use the mystery lemma:

import topology.algebra.module

open_locale pointwise

variables {α : Type*} [topological_space α] [add_comm_group α] [has_continuous_add α]

lemma interior_add_interior_subset {s t : set α} :
  interior s + interior t ⊆ interior (s + t) :=
begin
  rw subset_interior_iff_subset_of_open,
  { rintros x ⟨a, b, ha, hb, rfl⟩,
    exact set.add_mem_add (interior_subset ha) (interior_subset hb) },
  { rw ← set.Union_add_left_image,
    apply is_open_bUnion,
    intros x hx,
    refine (homeomorph.add_left x).is_open_map _ _,
    exact is_open_interior }
end

[Heather Macbeth]

That one will actually show that s + interior t ⊆ interior (s + t) or vice versa.

[Yaël Dillies]

Is there some more general result about open maps α × α → α?

[Anatole Dedecker]

I'm not at my computer so I can't golf, but I think there should be a one or two line proof using docs#is_open.add_left, docs#interior_maximal and docs#set.add_subset_add

[Pascal Schoppenhauer]

@Heather Macbeth Hey I'm sorry to bother you, but I'm still very new to Lean and I would like to understand what the "rintros" command does. I have seen it in many simple examples but I can't find a good explanation of what its purpose is.

[Eric Wieser]

tactic#rintro might be helpful (rintros is the same as rintro)