subtype function

Stream: new members

[Victor Porton]

We know

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

[Kyle Miller]

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]

Actually, is that c y another hypothesis?

[Kyle Miller]

I assume so, so here:

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

[Victor Porton]

Yes, c y is a hypothesis.

[Kyle Miller]

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]

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.