Open set of reals contains ball/interval

Stream: Is there code for X?

[Bhavik Mehta]

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]

Presumably docs#nhds_basis_ball ? :down:

[Kevin Buzzard]

docs#metric.is_open_iff ?

[Kevin Buzzard]

(or go via neighbourhood filters)

[Bhavik Mehta]

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

[Kevin Buzzard]

linarith is your friend now

[Bhavik Mehta]

It can't seem to handle the dist

[Kevin Buzzard]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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]

That's surprisingly long for an "obvious" statement

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

closed_ball_Icc made it a bit nicer at least

[Anatole Dedecker]

Would docs#metric.closed_ball_subset_ball help you ?

[Bhavik Mehta]

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

[Bhavik Mehta]

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]

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

[Damiano Testa]

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]

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]

Ahh this is great Shing, thanks so much!

[Yaël Dillies]

Do we still not have a version of docs#metric.is_open_iff for closed_ball?

[Bhavik Mehta]

it's easy to prove:

lemma yael {α : Type*} [pseudo_metric_space α] {s : set α} :
  is_open s ↔ ∀ x ∈ s, (∃ ε > 0, metric.closed_ball x ε ⊆ s) :=
by simp only [is_open_iff_mem_nhds, metric.nhds_basis_closed_ball.mem_iff]

essentially the same as docs#metric.is_open_iff

[Yaël Dillies]

So I assume the answer is "no" :grinning:

[Sebastien Gouezel]

We have it but in greater generality, by saying that closed balls form a basis of the neighborhoods of a point, and then you deduce whatever you like from general properties of bases.