Zulip Chat Archive

Stream: Is there code for X?

Topic: Open set of reals contains ball/interval


view this post on Zulip 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

view this post on Zulip Adam Topaz (Apr 15 2021 at 13:58):

Presumably docs#nhds_basis_ball ? :down:

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 13:59):

docs#metric.is_open_iff ?

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 14:00):

(or go via neighbourhood filters)

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 14:01):

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

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 14:02):

linarith is your friend now

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 14:02):

It can't seem to handle the dist

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 14:03):

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

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 14:04):

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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 14:05):

That's surprisingly long for an "obvious" statement

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 14:08):

closed_ball_Icc made it a bit nicer at least

view this post on Zulip Anatole Dedecker (Apr 15 2021 at 14:09):

Would docs#metric.closed_ball_subset_ball help you ?

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 14:09):

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

view this post on Zulip 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

view this post on Zulip Anatole Dedecker (Apr 15 2021 at 14:10):

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

view this post on Zulip 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,

view this post on Zulip 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ε₂

view this post on Zulip 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