# Zulip Chat Archive

## Stream: general

### Topic: mem_of_super_set

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

This time I ask before refactoring: should we add

```
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):

I'm talking about my suggestion.

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

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

Sorry, I need to go now. I'll return tonight.

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