## Stream: general

### Topic: mem_of_super_set

#### Patrick Massot (Aug 13 2021 at 12:36):

import order.filter.basic

open filter

lemma has_mem.mem.up {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y) : y ∈ f :=
mem_of_superset hx h

example {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y) : y ∈ f :=
hx.up h


If yes, what would be a good name? up is very short, but is it clear enough?

#### Patrick Massot (Aug 13 2021 at 12:37):

This lemma is used a lot.

#### Eric Wieser (Aug 13 2021 at 13:23):

It feels a bit weird to put dot notation on has_mem.mem that only applies to one particular instance of has_mem

#### Eric Wieser (Aug 13 2021 at 13:33):

Here's a neat trick that doesn't prevent other types defining a different meaning of has_mem.up:

import order.filter.basic

open filter

/-- Alias for dot notation -/
abbreviation filter_mem_dot_notation (P : Prop) : Prop := P

-- wrap the resulting Prop in a type alias for dot notation
instance filter.has_mem' {α : Type*} : has_mem (set α) (filter α) :=
{mem := λ u f, filter_mem_dot_notation (u ∈ f.sets) }

--note: for dot notation, hx is wrapped.
lemma filter_mem_dot_notation.up {α : Type*} {f : filter α} {x y : set α}
(hx : filter_mem_dot_notation (x ∈ f)) (h : x ⊆ y) : y ∈ f :=
sorry

-- result: dot notation that is specific to filter.has_mem
example {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y) : y ∈ f :=
hx.up h


(edit: split the discussion about error message weirdness to a new thread)

#### Patrick Massot (Aug 13 2021 at 13:43):

This weirdness is the reason why it wasn't done before, but it actually causes no harm (and I think we recently did the same for other similar cases).

#### Eric Wieser (Aug 13 2021 at 13:44):

I'm not sure I understand; are you saying that your original has_mem.mem.up causes no harm, or that my revised solution that doesn't produce the weird error causes no harm?

#### Patrick Massot (Aug 13 2021 at 13:45):

But if yours works and does not leak anywhere then it's ok.

#### Eric Wieser (Aug 13 2021 at 13:49):

Just checking you weren't saying that we'd already used the trick I suggest elsewhere. Can you come up with a similar case for the approach you suggest? It might be worth assembling a list of things like has_mem.mem.up, so that in future someone can try the dot notation hack I suggest above in lots of places at once, in order to increase the chance of finding leaks.

#### Kyle Miller (Aug 13 2021 at 17:06):

Would it still work if it were put on has_subset.subset instead? I like thinking of this fact as being functorial in h.

lemma has_subset.subset.up {α : Type*} {f : filter α} {x y : set α} (h : x ⊆ y) (hx : x ∈ f) : y ∈ f


To make this more general, there could be a typeclass to introduce has_subset.subset.up functors:

import order.filter.basic

open filter

class has_subset_up (α : Type*) [has_subset α] (β : α → Sort*) :=
(up : Π {x y : α}, x ⊆ y → β x → β y)

lemma has_subset.subset.up {α : Type*} [has_subset α] {β : α → Sort*} [has_subset_up α β]
{x y : α}
(h : x ⊆ y) (hx : β x) : β y :=
has_subset_up.up h hx

instance filter.subset_up {α : Type*} (f : filter α) : has_subset_up (set α) (∈f) :=
{ up := λ x y h hx, mem_of_superset hx h }

example {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y) : y ∈ f :=
h.up hx


Or there could be a more specialized version of this:

import order.filter.basic

open filter

class has_subset_up (α : out_param \$ Type*) (β : Type*) [has_mem α β] [has_subset α] :=
(up : ∀ {x y : α} {z : β}, x ⊆ y → x ∈ z → y ∈ z)

lemma has_subset.subset.up {α : Type*} {β : Type*} [has_mem α β] [has_subset α] [has_subset_up α β]
{x y : α} {z : β}
(h : x ⊆ y) (hx : x ∈ z) : y ∈ z :=
has_subset_up.up h hx

instance {α : Type*} : has_subset_up (set α) (filter α) :=
{ up := λ x y z h hx, mem_of_superset hx h }

example {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y) : y ∈ f :=
h.up hx


#### Eric Wieser (Aug 13 2021 at 18:37):

The typeclass approach is probably more sensible than the type alias approach I suggested. Can you think of a second instance, or is the only place this happens on filters anyway?

#### Kyle Miller (Aug 13 2021 at 18:53):

instance subtype.subset_up {α : Type*} : has_subset_up (set α) (λ s, s) :=
{ up := λ x y, set.inclusion }

example {α : Type*} (x y : set α) (h : x ⊆ y) (a : x) : y := h.up a


#### Kyle Miller (Aug 13 2021 at 18:59):

I can't get it to work where up gives structured functions, like homomorphisms. The subset relation for subobjects giving homomorphisms between their coercions to types could have been another use.

#### Kyle Miller (Aug 13 2021 at 19:02):

What I tried was

class has_subset_up (α : Type*) [has_subset α] (β : α → α → Sort*) :=
(up : Π {x y : α}, x ⊆ y → β x y)


but then h.up a is "too many arguments"

#### Eric Wieser (Aug 13 2021 at 19:23):

 β should be an outparam, right?

#### Kyle Miller (Aug 13 2021 at 19:25):

Do you mean in this version?

class has_subset_up (α : Type*) [has_subset α] (β : α → Sort*) :=
(up : Π {x y : α}, x ⊆ y → β x → β y)


It's not an out_param because subset-of relations can have multiple induced maps. set α can have one for both filter and subtype.

#### Patrick Massot (Aug 13 2021 at 19:36):

All this is a lot of fun but it really smells over-engineering until we have a second lemma that would use it.

#### Patrick Massot (Aug 13 2021 at 19:36):

My original suggestion works without any type class search or tricky aliasing.

#### Kyle Miller (Aug 13 2021 at 19:48):

@Patrick Massot Is there any reason the filter lemma couldn't be has_subset.subset.up? Another possible name is has_subset.subset.map, though I don't think there's much of a reason to prefer that over up.

#### Patrick Massot (Aug 13 2021 at 19:49):

I don't care about attaching it to has_mem vs has_subset, both would make sense.

Last updated: Aug 03 2023 at 10:10 UTC