## Stream: maths

### Topic: set.not_mem_Inter_iff

#### 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?

#### Kevin Buzzard (Jan 13 2020 at 22:08):

It would be a convenient thing for me to rewrite.

#### Joe (Jan 13 2020 at 22:21):

I think you can just rewrite mem_Inter

#### 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]


#### Kevin Buzzard (Jan 13 2020 at 22:24):

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

haha, thanks.

#### Kevin Buzzard (Jan 13 2020 at 22:32):

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

#### 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?

#### 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