## Stream: Is there code for X?

### Topic: Open set of reals contains ball/interval

#### Bhavik Mehta (Apr 15 2021 at 13:54):

I'm struggling to find something of this form, though I'm sure it's there somewhere:

import data.real.basic
import topology.algebra.ordered
import topology.instances.real

noncomputable theory
open set

example {S : set ℝ} (hS₁ : is_open S) (x : ℝ) (hS₂ : x ∈ S) :
∃ (r:ℝ), 0 < r ∧ ∃ (r:ℝ), 0 < r ∧ Icc (x-r) (x+r) ⊆ S :=
begin

end


#### Adam Topaz (Apr 15 2021 at 13:58):

Presumably docs#nhds_basis_ball ? :down:

#### Kevin Buzzard (Apr 15 2021 at 14:00):

(or go via neighbourhood filters)

#### Bhavik Mehta (Apr 15 2021 at 14:01):

Now I have a goal of the form Icc (x - ε / 2) (x + ε / 2) ⊆ metric.ball x ε

#### Kevin Buzzard (Apr 15 2021 at 14:02):

linarith is your friend now

#### Bhavik Mehta (Apr 15 2021 at 14:02):

It can't seem to handle the dist

#### Kevin Buzzard (Apr 15 2021 at 14:03):

oh I think it's defeq to abs so maybe you need to unfold abs?

#### Bhavik Mehta (Apr 15 2021 at 14:04):

rw real.dist_eq did that, but now linarith can't handle the abs

#### Bhavik Mehta (Apr 15 2021 at 14:04):

Alright here's what I ended up with

example {S : set ℝ} (hS₁ : is_open S) (x : ℝ) (hS₂ : x ∈ S) :
∃ (r:ℝ), 0 < r ∧ Icc (x-r) (x+r) ⊆ S :=
begin
rw metric.is_open_iff at hS₁,
obtain ⟨ε, hε₁, hε₂⟩ := hS₁ x hS₂,
refine ⟨ε/2, half_pos hε₁, _⟩,
apply set.subset.trans _ hε₂,
intros y hy,
simp only [real.dist_eq, abs_sub_lt_iff, exists_prop, metric.mem_ball, gt_iff_lt, mem_Icc] at *,
split;
linarith,
end


#### Bhavik Mehta (Apr 15 2021 at 14:05):

That's surprisingly long for an "obvious" statement

#### Bhavik Mehta (Apr 15 2021 at 14:06):

example {S : set ℝ} (hS₁ : is_open S) (x : ℝ) (hS₂ : x ∈ S) :
∃ (r:ℝ), 0 < r ∧ Icc (x-r) (x+r) ⊆ S :=
begin
rw metric.is_open_iff at hS₁,
obtain ⟨ε, hε₁, hε₂⟩ := hS₁ x hS₂,
refine ⟨ε/2, half_pos hε₁, _⟩,
rw ←closed_ball_Icc,
apply set.subset.trans (metric.closed_ball_subset_ball (half_lt_self hε₁)) hε₂,
end


Golfed a bit to this

#### Kevin Buzzard (Apr 15 2021 at 14:07):

I think we've missed some library function. I think I've struggled to find this before.

#### Bhavik Mehta (Apr 15 2021 at 14:08):

closed_ball_Icc made it a bit nicer at least

#### Bhavik Mehta (Apr 15 2021 at 14:09):

That's what I used in the golfed version, it did help!

#### Bhavik Mehta (Apr 15 2021 at 14:10):

It's working in my actual case too now - thanks everyone! It was closed_ball_Icc together with metric.is_open_iff that were the things I couldn't find

#### Anatole Dedecker (Apr 15 2021 at 14:10):

Oh indeed, I should have read it with more attention :sweat_smile:

#### Damiano Testa (Apr 15 2021 at 14:14):

Maybe the interval thing can also be simplified with

  have : S ∈ nhds x,exact mem_nhds_sets hS₁ hS₂,
obtain F := mem_nhds_iff_exists_Ioo_subset.mp this,


#### Shing Tak Lam (Apr 15 2021 at 14:22):

import data.real.basic
import topology.algebra.ordered
import topology.instances.real

noncomputable theory
open set

example {S : set ℝ} (hS₁ : is_open S) (x : ℝ) (hS₂ : x ∈ S) :
∃ (r:ℝ), 0 < r ∧ Icc (x-r) (x+r) ⊆ S :=
let ⟨ε, hε₁, hε₂⟩ :=
((@metric.nhds_basis_closed_ball _ _ x).1 _).1 ((is_open_iff_mem_nhds.1 hS₁) x hS₂) in
⟨ε, hε₁, @closed_ball_Icc x ε ▸ hε₂⟩


#### Bhavik Mehta (Apr 15 2021 at 14:26):

Ahh this is great Shing, thanks so much!

Last updated: May 16 2021 at 05:21 UTC