UnivLE

📁 Source: Mathlib/Logic/UnivLE.lean

Statistics

Metric	Count
Definitions	0
Theorems trans_univLE, self, small, succ, trans, zero, univLE_iff, univLE_max, univLE_of_max	9
Total	9

Small

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trans_univLE 📖	mathematical	—	Small	—	equiv_small UnivLE.small

UnivLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
self 📖	mathematical	—	UnivLE	—	small_self
small 📖	mathematical	—	Small	—	—
succ 📖	mathematical	—	UnivLE	—	trans small_succ
trans 📖	mathematical	—	UnivLE	—	Small.trans_univLE small
zero 📖	mathematical	—	UnivLE	—	small_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
univLE_iff 📖	mathematical	—	UnivLE Small	—	—
univLE_max 📖	mathematical	—	UnivLE	—	small_max
univLE_of_max 📖	mathematical	—	UnivLE	—	UnivLE.trans univLE_max

---

← Back to Index