Lattice

📁 Source: Mathlib/RingTheory/Finiteness/Lattice.lean

Statistics

Metric	Count
Definitions	0
Theorems finite_iSup	1
Total	1

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_iSup 📖	mathematical	Module.Finite Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike addCommMonoid module	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	nonempty_fintype instFinitePLift iSup_plift_down Finset.sup_univ_eq_iSup finite_finset_sup

---

← Back to Index