Zulip Chat Archive

Stream: maths

Topic: open subset of the reals


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

view this post on Zulip Bhavik Mehta (Jul 07 2020 at 20:48):

Am I using these things correctly?

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:48):

apply is misbehaving

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:48):

messing up tc search

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:49):

Try exact

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:49):

(or refine)

view this post on Zulip Bhavik Mehta (Jul 07 2020 at 20:49):

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

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

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:50):

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

view this post on Zulip Bhavik Mehta (Jul 07 2020 at 20:50):

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

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:53):

It doesn't seem to be.

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

view this post on Zulip Reid Barton (Jul 07 2020 at 23:34):

This is the usual apply bug

view this post on Zulip Reid Barton (Jul 07 2020 at 23:35):

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

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

view this post on Zulip Bhavik Mehta (Jul 07 2020 at 23:50):

again refine works but apply doesn't

view this post on Zulip Reid Barton (Jul 07 2020 at 23:51):

same issue

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

view this post on Zulip Reid Barton (Jul 07 2020 at 23:55):

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

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

view this post on Zulip Reid Barton (Jul 07 2020 at 23:56):

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

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

am I misreading this then?

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

view this post on Zulip Reid Barton (Jul 07 2020 at 23:57):

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

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

view this post on Zulip Reid Barton (Jul 07 2020 at 23:57):

same for <= versus subset which is a Pi type

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