Congruence

📁 Source: Mathlib/Order/Lattice/Congruence.lean

Statistics

Metric	Count
Definitions LatticeCon, ker, mk', toSetoid	4
Theorems inf, ker_r, r_inf_sup_iff, sup	4
Total	8

LatticeCon

Definitions

Name	Category	Theorems
ker 📖	CompOp	1 math math: ker_r
mk' 📖	CompOp	—
toSetoid 📖	CompOp	2 math math: r_inf_sup_iff, ker_r

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf 📖	mathematical	toSetoid	SemilatticeInf.toMin Lattice.toSemilatticeInf	—	—
ker_r 📖	mathematical	—	toSetoid ker Function.onFun DFunLike.coe	—	—
r_inf_sup_iff 📖	mathematical	—	toSetoid SemilatticeInf.toMin Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	inf_of_le_left inf_of_le_right inf sup_of_le_left sup
sup 📖	mathematical	toSetoid	SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—

(root)

Definitions

Name	Category	Theorems
LatticeCon 📖	CompData	—

---

← Back to Index