OfFun

📁 Source: Mathlib/Topology/UniformSpace/OfFun.lean

Statistics

Metric	Count
Definitions ofFun, ofFunOfHasBasis	2
Theorems hasBasis_ofFun	1
Total	3

UniformSpace

Definitions

Name	Category	Theorems
ofFun 📖	CompOp	1 math math: hasBasis_ofFun
ofFunOfHasBasis 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasBasis_ofFun 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLE AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	Filter.HasBasis uniformity ofFun setOf	—	Filter.hasBasis_biInf_principal' lt_min lt_of_lt_of_le min_le_left min_le_right

---

← Back to Index