## Stream: new members

### Topic: subtype function

#### Victor Porton (Apr 02 2022 at 00:49):

We know

• α β: Type
• c: set α
• f: ({x:α // c x} → β)
• y: α
• c y
How to apply f to y?

#### Kyle Miller (Apr 02 2022 at 00:51):

By the way, writing a #mwe like the following makes it easier for everyone:

example (α β: Type) (c: set α) (y: α) (f: ({x:α // c x} → β)) : c y := sorry


(That way we don't have a bunch of people collectively spending time writing what I just did.)

#### Kyle Miller (Apr 02 2022 at 00:52):

Actually, is that c y another hypothesis?

#### Kyle Miller (Apr 02 2022 at 00:53):

I assume so, so here:

example (α β: Type) (c: set α) (y: α) (f: ({x:α // c x} → β)) (h : c y) : β := f ⟨y, h⟩


#### Victor Porton (Apr 02 2022 at 00:53):

Yes, c y is a hypothesis.

#### Kyle Miller (Apr 02 2022 at 00:54):

This is equivalent:

example (α β: Type) (c: set α) (y: α) (f: c → β) (h : y ∈ c) : β := f ⟨y, h⟩


When you use set, you're meant to use ∈ since there are simp lemmas that are for sets that won't apply if you use c as a predicate directly.

#### Kyle Miller (Apr 02 2022 at 00:55):

The angle brackets ("anonymous constructor notation") are short for

example (α β: Type) (c: set α) (y: α) (f: c → β) (h : y ∈ c) : β := f (subtype.mk y h)


and I'm able to use c in the domain of f since Lean will automatically coerce it to a type using subtype.

Last updated: Dec 20 2023 at 11:08 UTC