# Zulip Chat Archive

## 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 13:59):

#### 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

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

Would docs#metric.closed_ball_subset_ball help you ?

#### 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