Zulip Chat Archive

Stream: maths

Topic: open subset of the reals

Bhavik Mehta (Jul 07 2020 at 20:47):

Why does this not work? Also, library_search and suggest don't work here either...

import topology.opens
import topology.instances.real
import tactic

open topological_space
namespace topological_space.opens

noncomputable theory

example : opens ℝ :=
begin
  refine ⟨set.Ioo 0 1, _⟩,
  apply is_open_Ioo,
end

end topological_space.opens

Bhavik Mehta (Jul 07 2020 at 20:48):

Am I using these things correctly?

Patrick Massot (Jul 07 2020 at 20:48):

apply is misbehaving

Patrick Massot (Jul 07 2020 at 20:48):

messing up tc search

Patrick Massot (Jul 07 2020 at 20:49):

Try exact

Patrick Massot (Jul 07 2020 at 20:49):

(or refine)

Bhavik Mehta (Jul 07 2020 at 20:49):

Weird, I'm on a version of mathlib from today

Bhavik Mehta (Jul 07 2020 at 20:49):

It's more frustrating that library search didn't work, I had to go searching through topology/algebra to find this name

Patrick Massot (Jul 07 2020 at 20:50):

Everybody is. Who would want to be lagging so much?

Bhavik Mehta (Jul 07 2020 at 20:50):

So this isn't the recent apply bug that got fixed?

Patrick Massot (Jul 07 2020 at 20:53):

It doesn't seem to be.

Patrick Massot (Jul 07 2020 at 22:01):

I tried pretty hard but I haven't been able to reproduce this bug outside mathlib. @Gabriel Ebner do you have anything to say about

import topology.instances.real

#check  @is_open_Ioo

example : is_open (set.Ioo 0 1 : set ℝ)  :=
begin
  -- apply is_open_Ioo, -- fails
  exact is_open_Ioo, -- works
end

Reid Barton (Jul 07 2020 at 23:34):

This is the usual apply bug

Reid Barton (Jul 07 2020 at 23:35):

openness for a subset of real is presumably a Pi type of some kind

Bhavik Mehta (Jul 07 2020 at 23:50):

There's also

import topology.opens
import topology.instances.real
import tactic

open topological_space
open set

namespace topological_space

noncomputable theory

example (P Q : opens ℝ) : P ⊓ Q ≤ P :=
begin
  apply inf_le_left,
end

end topological_space

Bhavik Mehta (Jul 07 2020 at 23:50):

again refine works but apply doesn't

Reid Barton (Jul 07 2020 at 23:51):

same issue

Bhavik Mehta (Jul 07 2020 at 23:51):

and same, without the real:

import topology.opens

namespace topological_space

example (U : Type*) [topological_space U] (P Q : opens U) : P ⊓ Q ≤ P :=
begin
  apply inf_le_left,
end

end topological_space