Interior of a set-level

Stream: Is there code for X?

[Yaël Dillies]

Do we something along those lines?

import topology.algebra.ordered.basic

lemma interior_le {α β : Type*} [topological_space α] [linear_order α] [order_closed_topology α]
  [topological_space β] [linear_order β] [order_closed_topology β] {f g : β → α} (hf : continuous f)
  (hg : continuous g) :
  {b | f b < g b} ⊆ interior {b | f b ≤ g b}

I am not sure about the correct typeclasses.

[Heather Macbeth]

A possible simplification (if indeed my foo is true):

import topology.algebra.ordered.basic

variables {α : Type*} [topological_space α] [linear_order α] [order_closed_topology α]

lemma foo : {p : α × α | p.1 < p.2} ⊆ interior {p | p.1 ≤ p.2} := sorry

lemma interior_le {β : Type*} [topological_space β] [linear_order β] [order_closed_topology β]
  {f g : β → α} (hf : continuous f) (hg : continuous g) :
  {b | f b < g b} ⊆ interior {b | f b ≤ g b} :=
begin
  let F : β → α × α := λ b, (f b, g b),
  show F ⁻¹' {p : α × α | p.1 < p.2} ⊆ interior (F ⁻¹' {p | p.1 ≤ p.2}),
  refine (set.preimage_mono foo).trans _,
  refine preimage_interior_subset_interior_preimage (hf.prod_mk hg),
end

[Heather Macbeth]

Ah, indeed foo is true.

lemma foo : {p : α × α | p.1 < p.2} ⊆ interior {p | p.1 ≤ p.2} :=
begin
  rw subset_interior_iff_subset_of_open,
  { rintros p (hp : p.1 < p.2),
    exact hp.le },
  { exact is_open_lt_prod }
end

[Heather Macbeth]

And in fact we have a more elaborate pre-build lemma next to docs#is_open_lt_prod, namely docs#is_open_lt, which is basically what you originally asked for:

lemma interior_le {β : Type*} [topological_space β] [linear_order β] [order_closed_topology β]
  {f g : β → α} (hf : continuous f) (hg : continuous g) :
  {b | f b < g b} ⊆ interior {b | f b ≤ g b} :=
begin
  rw subset_interior_iff_subset_of_open,
  { rintros p (hp : f p < g p),
    exact hp.le },
  { exact is_open_lt hf hg }
end

[Yaël Dillies]

Uh, I knew about is_open_lt but I couldn't get it to work in this case :sweat_smile: