Zulip Chat Archive

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