set.not_mem_Inter_iff

Stream: maths

[Kevin Buzzard]

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]

It would be a convenient thing for me to rewrite.

[Joe]

I think you can just rewrite mem_Inter

[Joe]

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]

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

[Joe]

haha, thanks.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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