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

(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

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


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

same issue, it doesn't have anything to do with real

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

Oh so it's that openness for a subset in general is a Pi type, not just for the usual topology on R?

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

no, it's precisely because openness in general is not a Pi type

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

Reid Barton said:

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

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

it happens when specializing the lemma to the relevant type(s) causes it to grow more ->s in its type, usually because of a type class instance

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

openness in general is not a Pi type, it's a field of a variable (topology)

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

but in the topology on real (and lots of other specific examples) that field is defined as a Pi type

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

same for <= versus subset which is a Pi type

Kenny Lau (Jul 08 2020 at 05:15):

the standard workaround seems to be apply' is_open_Ioo,

Last updated: May 11 2021 at 00:31 UTC