TwoPointing

Statistics

Metric	Count
Definitions `TwoPointing`, `bool`, `instInhabitedBool`, `pi`, `prod`, `prop`, `sum`, `swap`, `toProd`, `instDecidableEqTwoPointing`, `decEq`	11
Theorems `bool_fst`, `bool_snd`, `ext`, `ext_iff`, `fst_ne_snd`, `instNonemptyOfNontrivial`, `nonempty_two_pointing_iff`, `pi_fst`, `pi_snd`, `prod_fst`, `prod_snd`, `prop_fst`, `prop_snd`, `snd_ne_fst`, `sum_fst`, `sum_snd`, `swap_fst`, `swap_snd`, `swap_swap`, `swap_toProd`, `to_nontrivial`	21
Total	32

Name	Category	Theorems
`bool` 📖	CompOp	2 math math: `bool_snd`, `bool_fst`
`instInhabitedBool` 📖	CompOp	—
`pi` 📖	CompOp	2 math math: `pi_fst`, `pi_snd`
`prod` 📖	CompOp	2 math math: `prod_snd`, `prod_fst`
`prop` 📖	CompOp	2 math math: `prop_snd`, `prop_fst`
`sum` 📖	CompOp	2 math math: `sum_fst`, `sum_snd`
`swap` 📖	CompOp	8 math math: `swap_swap`, `swap_toProd`, `swap_fst`, `TwoP.swapEquiv_functor_map_hom_toFun`, `TwoP.swap_obj_toTwoPointing`, `TwoP.swap_map`, `swap_snd`, `TwoP.swapEquiv_inverse_map_hom_toFun`
`toProd` 📖	CompOp	18 math math: `pointedToTwoPFst_obj_toTwoPointing_toProd`, `swap_toProd`, `prop_snd`, `swap_fst`, `prop_fst`, `prod_snd`, `sum_fst`, `bool_snd`, `bool_fst`, `TwoP.swapEquiv_functor_obj_toTwoPointing_toProd`, `pi_fst`, `sum_snd`, `swap_snd`, `ext_iff`, `TwoP.swapEquiv_inverse_obj_toTwoPointing_toProd`, `pi_snd`, `prod_fst`, `pointedToTwoPSnd_obj_toTwoPointing_toProd`

Name	Kind	Assumes	Proves	Validates	Depends On
`bool_fst` 📖	mathematical	—	`toProd` `bool`	—	—
`bool_snd` 📖	mathematical	—	`toProd` `bool`	—	—
`ext` 📖	—	`toProd`	—	—	—
`ext_iff` 📖	mathematical	—	`toProd`	—	`ext`
`fst_ne_snd` 📖	—	—	—	—	—
`instNonemptyOfNontrivial` 📖	mathematical	—	`TwoPointing`	—	`exists_pair_ne`
`nonempty_two_pointing_iff` 📖	mathematical	—	`TwoPointing` `Nontrivial`	—	`to_nontrivial` `instNonemptyOfNontrivial`
`pi_fst` 📖	mathematical	—	`toProd` `pi`	—	—
`pi_snd` 📖	mathematical	—	`toProd` `pi`	—	—
`prod_fst` 📖	mathematical	—	`toProd` `prod`	—	—
`prod_snd` 📖	mathematical	—	`toProd` `prod`	—	—
`prop_fst` 📖	mathematical	—	`toProd` `prop`	—	—
`prop_snd` 📖	mathematical	—	`toProd` `prop`	—	—
`snd_ne_fst` 📖	—	—	—	—	`fst_ne_snd`
`sum_fst` 📖	mathematical	—	`toProd` `sum`	—	—
`sum_snd` 📖	mathematical	—	`toProd` `sum`	—	—
`swap_fst` 📖	mathematical	—	`toProd` `swap`	—	—
`swap_snd` 📖	mathematical	—	`toProd` `swap`	—	—
`swap_swap` 📖	mathematical	—	`swap`	—	—
`swap_toProd` 📖	mathematical	—	`toProd` `swap`	—	—
`to_nontrivial` 📖	mathematical	—	`Nontrivial`	—	`fst_ne_snd`

Name	Category	Theorems
`TwoPointing` 📖	CompData	2 math math: `TwoPointing.nonempty_two_pointing_iff`, `TwoPointing.instNonemptyOfNontrivial`
`instDecidableEqTwoPointing` 📖	CompOp	—

Name	Category	Theorems
`decEq` 📖	CompOp	—

---