ULift

Statistics

Metric	Count
Definitions `instBEq_mathlib`, `instCompl`, `instLE_mathlib`, `instLT_mathlib`, `instMax_mathlib`, `instMin_mathlib`, `instOrd_mathlib`, `instPartialOrder`, `instPreorder`, `instSDiff_mathlib`	10
Theorems `down_beq`, `down_compare`, `down_compl`, `down_inf`, `down_le`, `down_lt`, `down_sdiff`, `down_sup`, `instLawfulBEqOrd_mathlib`, `instLawfulBOrd_mathlib`, `instLawfulLEOrd_mathlib`, `instLawfulLTOrd_mathlib`, `instOrientedOrd_mathlib`, `instTransOrd_mathlib`, `up_beq`, `up_compare`, `up_compl`, `up_inf`, `up_le`, `up_lt`, `up_sdiff`, `up_sup`	22
Total	32

ULift

Definitions

Name	Category	Theorems
`instBEq_mathlib` 📖	CompOp	4 math math: `instLawfulBOrd_mathlib`, `down_beq`, `instLawfulBEqOrd_mathlib`, `up_beq`
`instCompl` 📖	CompOp	2 math math: `up_compl`, `down_compl`
`instLE_mathlib` 📖	CompOp	6 math math: `orderIso_symm_apply_down`, `instLawfulBOrd_mathlib`, `down_le`, `up_le`, `orderIso_apply`, `instLawfulLEOrd_mathlib`
`instLT_mathlib` 📖	CompOp	6 math math: `instLawfulBOrd_mathlib`, `down_lt`, `up_lt`, `instWellFoundedLT`, `instLawfulLTOrd_mathlib`, `instWellFoundedGT`
`instMax_mathlib` 📖	CompOp	2 math math: `up_sup`, `down_sup`
`instMin_mathlib` 📖	CompOp	2 math math: `down_inf`, `up_inf`
`instOrd_mathlib` 📖	CompOp	8 math math: `up_compare`, `instLawfulBOrd_mathlib`, `instLawfulLTOrd_mathlib`, `instLawfulBEqOrd_mathlib`, `instTransOrd_mathlib`, `down_compare`, `instLawfulLEOrd_mathlib`, `instOrientedOrd_mathlib`
`instPartialOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	7 math math: `OrderHom.uliftLeftMap_uliftRightMap_eq`, `SSet.stdSimplex.isoNerve_hom_app_apply`, `OrderHom.uliftRightMap_uliftLeftMap_eq`, `OrderHom.uliftMap_coe_down`, `OrderHom.uliftLeftMap_coe`, `OrderHom.uliftRightMap_coe_down`, `SSet.stdSimplex.isoNerve_inv_app_apply`
`instSDiff_mathlib` 📖	CompOp	2 math math: `down_sdiff`, `up_sdiff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_beq` 📖	mathematical	—	`instBEq_mathlib`	—	—
`down_compare` 📖	mathematical	—	`instOrd_mathlib`	—	—
`down_compl` 📖	mathematical	—	`Compl.compl` `instCompl`	—	—
`down_inf` 📖	mathematical	—	`instMin_mathlib`	—	—
`down_le` 📖	mathematical	—	`instLE_mathlib`	—	—
`down_lt` 📖	mathematical	—	`instLT_mathlib`	—	—
`down_sdiff` 📖	mathematical	—	`instSDiff_mathlib`	—	—
`down_sup` 📖	mathematical	—	`instMax_mathlib`	—	—
`instLawfulBEqOrd_mathlib` 📖	mathematical	—	`instBEq_mathlib` `instOrd_mathlib`	—	—
`instLawfulBOrd_mathlib` 📖	mathematical	—	`instLE_mathlib` `instLT_mathlib` `instBEq_mathlib` `instOrd_mathlib`	—	`instTransOrd_mathlib` `instLawfulBEqOrd_mathlib`
`instLawfulLEOrd_mathlib` 📖	mathematical	—	`instLE_mathlib` `instOrd_mathlib`	—	`instOrientedOrd_mathlib`
`instLawfulLTOrd_mathlib` 📖	mathematical	—	`instLT_mathlib` `instOrd_mathlib`	—	`instOrientedOrd_mathlib`
`instOrientedOrd_mathlib` 📖	mathematical	—	`instOrd_mathlib`	—	—
`instTransOrd_mathlib` 📖	mathematical	—	`instOrd_mathlib`	—	`instOrientedOrd_mathlib`
`up_beq` 📖	mathematical	—	`instBEq_mathlib`	—	—
`up_compare` 📖	mathematical	—	`instOrd_mathlib`	—	—
`up_compl` 📖	mathematical	—	`Compl.compl` `instCompl`	—	—
`up_inf` 📖	mathematical	—	`instMin_mathlib`	—	—
`up_le` 📖	mathematical	—	`instLE_mathlib`	—	—
`up_lt` 📖	mathematical	—	`instLT_mathlib`	—	—
`up_sdiff` 📖	mathematical	—	`instSDiff_mathlib`	—	—
`up_sup` 📖	mathematical	—	`instMax_mathlib`	—	—

---

← Back to Index