Fin

📁 Source: PhysLean/Mathematics/Fin.lean

Statistics

Metric	Count
Definitions `equivCons`, `finExtractOnPermHom`, `finExtractOne`, `finExtractOnePerm`, `finExtractTwo`, `finMapToEquiv`, `predAboveI`	7
Theorems `equivCons_castOrderIso`, `equivCons_succ`, `equivCons_symm_succ`, `equivCons_trans`, `equivCons_zero`, `finExtractOnPermHom_inv`, `finExtractOnePerm_apply`, `finExtractOnePerm_equiv`, `finExtractOnePerm_symm_apply`, `finExtractOne_apply_eq`, `finExtractOne_apply_neq`, `finExtractOne_symm_inl_apply`, `finExtractOne_symm_inr`, `finExtractOne_symm_inr_apply`, `finExtractTwo_apply_fst`, `finExtractTwo_apply_snd`, `finExtractTwo_symm_inl_inl_apply`, `finExtractTwo_symm_inl_inr_apply`, `finExtractTwo_symm_inr`, `finExtractTwo_symm_inr_apply`, `finMapToEquiv_apply`, `finMapToEquiv_symm_apply`, `finMapToEquiv_symm_eq`, `predAboveI_eq_iff`, `predAboveI_ge`, `predAboveI_lt`, `predAboveI_self`, `predAboveI_succAbove`, `succAbove_succAbove_predAboveI`, `succsAbove_predAboveI`	30
Total	37

PhysLean.Fin

Definitions

Name	Category	Theorems
`equivCons` 📖	CompOp	5 math math: `equivCons_trans`, `equivCons_castOrderIso`, `equivCons_succ`, `equivCons_zero`, `equivCons_symm_succ`
`finExtractOnPermHom` 📖	CompOp	1 math math: `finExtractOnPermHom_inv`
`finExtractOne` 📖	CompOp	7 math math: `finExtractOne_symm_inr_apply`, `finExtractOne_symm_inr`, `finExtractOne_apply_eq`, `finExtractOne_apply_neq`, `finExtractOnePerm_symm_apply`, `finExtractOnePerm_apply`, `finExtractOne_symm_inl_apply`
`finExtractOnePerm` 📖	CompOp	3 math math: `finExtractOnePerm_equiv`, `finExtractOnePerm_symm_apply`, `finExtractOnePerm_apply`
`finExtractTwo` 📖	CompOp	6 math math: `finExtractTwo_symm_inr`, `finExtractTwo_apply_fst`, `finExtractTwo_symm_inl_inl_apply`, `finExtractTwo_symm_inr_apply`, `finExtractTwo_apply_snd`, `finExtractTwo_symm_inl_inr_apply`
`finMapToEquiv` 📖	CompOp	3 math math: `finMapToEquiv_apply`, `finMapToEquiv_symm_eq`, `finMapToEquiv_symm_apply`
`predAboveI` 📖	CompOp	10 math math: `predAboveI_eq_iff`, `succsAbove_predAboveI`, `finExtractOne_apply_neq`, `predAboveI_ge`, `finExtractOnePerm_symm_apply`, `predAboveI_self`, `finExtractOnePerm_apply`, `predAboveI_lt`, `succAbove_succAbove_predAboveI`, `predAboveI_succAbove`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivCons_castOrderIso` 📖	mathematical	—	`equivCons`	—	—
`equivCons_succ` 📖	mathematical	—	`equivCons`	—	—
`equivCons_symm_succ` 📖	mathematical	—	`equivCons`	—	—
`equivCons_trans` 📖	mathematical	—	`equivCons`	—	—
`equivCons_zero` 📖	mathematical	—	`equivCons`	—	—
`finExtractOnPermHom_inv` 📖	mathematical	—	`finExtractOnPermHom`	—	`finExtractOne_symm_inr_apply` `predAboveI_lt` `predAboveI_succAbove` `predAboveI_ge`
`finExtractOnePerm_apply` 📖	mathematical	—	`finExtractOnePerm` `predAboveI` `finExtractOne`	—	—
`finExtractOnePerm_equiv` 📖	mathematical	—	`finExtractOnePerm`	—	`finExtractOne_symm_inr_apply` `succsAbove_predAboveI`
`finExtractOnePerm_symm_apply` 📖	mathematical	—	`finExtractOnePerm` `predAboveI` `finExtractOne`	—	—
`finExtractOne_apply_eq` 📖	mathematical	—	`finExtractOne`	—	—
`finExtractOne_apply_neq` 📖	mathematical	—	`finExtractOne` `predAboveI`	—	`finExtractOne_symm_inr_apply` `succsAbove_predAboveI`
`finExtractOne_symm_inl_apply` 📖	mathematical	—	`finExtractOne`	—	—
`finExtractOne_symm_inr` 📖	mathematical	—	`finExtractOne`	—	—
`finExtractOne_symm_inr_apply` 📖	mathematical	—	`finExtractOne`	—	`finExtractOne_symm_inr`
`finExtractTwo_apply_fst` 📖	mathematical	—	`finExtractTwo`	—	`finExtractOne_apply_eq`
`finExtractTwo_apply_snd` 📖	mathematical	—	`finExtractTwo`	—	`finExtractTwo_symm_inl_inr_apply`
`finExtractTwo_symm_inl_inl_apply` 📖	mathematical	—	`finExtractTwo`	—	—
`finExtractTwo_symm_inl_inr_apply` 📖	mathematical	—	`finExtractTwo`	—	`finExtractOne_symm_inl_apply` `finExtractOne_symm_inr_apply`
`finExtractTwo_symm_inr` 📖	mathematical	—	`finExtractTwo`	—	`finExtractTwo.eq_1` `finExtractOne_symm_inr_apply`
`finExtractTwo_symm_inr_apply` 📖	mathematical	—	`finExtractTwo`	—	`finExtractOne_symm_inr_apply`
`finMapToEquiv_apply` 📖	mathematical	—	`finMapToEquiv`	—	—
`finMapToEquiv_symm_apply` 📖	mathematical	—	`finMapToEquiv`	—	—
`finMapToEquiv_symm_eq` 📖	mathematical	—	`finMapToEquiv`	—	—
`predAboveI_eq_iff` 📖	mathematical	—	`predAboveI`	—	`succsAbove_predAboveI` `predAboveI_succAbove`
`predAboveI_ge` 📖	mathematical	—	`predAboveI`	—	—
`predAboveI_lt` 📖	mathematical	—	`predAboveI`	—	—
`predAboveI_self` 📖	mathematical	—	`predAboveI`	—	—
`predAboveI_succAbove` 📖	mathematical	—	`predAboveI`	—	—
`succAbove_succAbove_predAboveI` 📖	mathematical	—	`predAboveI`	—	`predAboveI_ge` `predAboveI_lt`
`succsAbove_predAboveI` 📖	mathematical	—	`predAboveI`	—	—

---

← Back to Index