Limit

📁 Source: Mathlib/Order/Interval/Set/Limit.lean

Statistics

Metric	Count
Definitions	0
Theorems isSuccLimit_coe	1
Total	1

Set.Ici

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSuccLimit_coe 📖	mathematical	Order.IsSuccLimit Set.Elem Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Subtype.preorder Set Set.instMembership	Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Ici	—	Set.not_isMin_coe not_covBy_iff LE.le.trans

---

← Back to Index