LocallyFinite

📁 Source: Mathlib/Order/UpperLower/LocallyFinite.lean

Statistics

Metric	Count
Definitions	0
Theorems lowerClosure, upperClosure	2
Total	2

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lowerClosure 📖	mathematical	—	Set.Finite SetLike.coe LowerSet Preorder.toLE LowerSet.instSetLike lowerClosure	—	coe_lowerClosure biUnion Set.finite_Iic
upperClosure 📖	mathematical	—	Set.Finite SetLike.coe UpperSet Preorder.toLE UpperSet.instSetLike upperClosure	—	coe_upperClosure biUnion Set.finite_Ici

---

← Back to Index