Documentation Verification Report

UnivLE

📁 Source: Mathlib/SetTheory/Cardinal/UnivLE.lean

Statistics

Metric	Count
Definitions `UnivLE`	1
Theorems `univLE_of_injective`, `univLE_iff_cardinal_le`, `univLE_iff_exists_embedding`, `univLE_total`	4
Total	5

Ordinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`univLE_of_injective` 📖	mathematical	`Ordinal`	`UnivLE`	—	`univLE_iff_exists_embedding`

(root)

Definitions

Name	Category	Theorems
`UnivLE` 📖	MathAb	13 math math: `univLE_iff_exists_embedding`, `UnivLE.succ`, `univLE_max`, `Ordinal.univLE_of_injective`, `univLE_iff_cardinal_le`, `UnivLE.trans`, `univLE_iff`, `UnivLE.self`, `UnivLE.zero`, `univLE_total`, `UnivLE.ofEssSurj`, `UnivLE_iff_essSurj`, `univLE_of_max`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`univLE_iff_cardinal_le` 📖	mathematical	—	`UnivLE` `Cardinal` `Cardinal.instLE` `Cardinal.univ`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `Mathlib.Tactic.Push.not_forall_eq` `LE.le.trans_lt` `Cardinal.lift_lift` `Cardinal.lift_univ` `Cardinal.lift_le` `Cardinal.univ_umax` `Cardinal.lift_lt_univ'` `Cardinal.lt_univ'` `Eq.le`
`univLE_iff_exists_embedding` 📖	mathematical	—	`UnivLE` `Function.Embedding` `Ordinal`	—	`univLE_iff_cardinal_le` `Cardinal.lift_mk_le'`
`univLE_total` 📖	mathematical	—	`UnivLE`	—	`le_total`

---

← Back to Index