Commit 2022-02-01 07:42 350ba8db

View on Github →

feat(data/two_pointing): Two pointings of a type (#11648) Define two_pointing α as the type of two pointings of α. This is a Type-valued structure version of nontrivial.

Estimated changes

Created src/data/two_pointing.lean

added theorem two_pointing.Prop_fst

added theorem two_pointing.Prop_snd

added theorem two_pointing.bool_fst

added theorem two_pointing.bool_snd

added theorem two_pointing.nonempty_two_pointing_iff

added def two_pointing.pi

added theorem two_pointing.pi_fst

added theorem two_pointing.pi_snd

added def two_pointing.prod

added theorem two_pointing.prod_fst

added theorem two_pointing.prod_snd

added theorem two_pointing.snd_ne_fst

added theorem two_pointing.sum_fst

added theorem two_pointing.sum_snd

added def two_pointing.swap

added theorem two_pointing.swap_fst

added theorem two_pointing.swap_snd

added theorem two_pointing.swap_swap

added theorem two_pointing.to_nontrivial

added structure two_pointing