Zulip Chat Archive

Stream: maths

Topic: set.not_mem_Inter_iff


view this post on Zulip Kevin Buzzard (Jan 13 2020 at 22:05):

Do we have this?

import data.set.lattice

def set.not_mem_Inter {X : Type*} {ι : Type*} (f : ι  set X) (x : X) :
(x   i, f i)   i : ι, x  f i := by finish

What's it called?

view this post on Zulip Kevin Buzzard (Jan 13 2020 at 22:08):

It would be a convenient thing for me to rewrite.

view this post on Zulip Joe (Jan 13 2020 at 22:21):

I think you can just rewrite mem_Inter

view this post on Zulip Joe (Jan 13 2020 at 22:21):

import data.set.lattice

noncomputable theory
open_locale classical

open set

def set.not_mem_Inter {X : Type*} {ι : Type*} (f : ι  set X) (x : X) :
(x   i, f i)   i : ι, x  f i := by rw [mem_Inter, not_forall]

view this post on Zulip Kevin Buzzard (Jan 13 2020 at 22:24):

Wow -- I am surprised that the rewrite works -- but it does!

view this post on Zulip Joe (Jan 13 2020 at 22:29):

haha, thanks.

view this post on Zulip Kevin Buzzard (Jan 13 2020 at 22:32):

It's hard for me to find where is defined.

view this post on Zulip Kevin Buzzard (Jan 13 2020 at 22:49):

aah, found it in core, and as I expected from your answer, it's notation. Line 347 of core.lean. I am still a bit surprised that rw can see through the notation -- oh -- so notation is just syntactic sugar?

view this post on Zulip Mario Carneiro (Jan 13 2020 at 23:06):

There is no not_mem constant for rw to see through - a ∉ b directly expands to not (a ∈ b)


Last updated: May 11 2021 at 17:39 UTC