Lattice

Statistics

Metric	Count
Definitions	0
Theorems `abs_apply`, `coe_abs`, `coe_mabs`, `instIsOrderedAddMonoid`, `instIsOrderedMonoid`, `mabs_apply`	6
Total	6

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `abs` `instLatticeOfTopologicalLattice` `instAddGroupOfIsTopologicalAddGroup`	—	—
`coe_abs` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `abs` `instLatticeOfTopologicalLattice` `instAddGroupOfIsTopologicalAddGroup` `Pi.instLattice` `Pi.addGroup`	—	—
`coe_mabs` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `mabs` `instLatticeOfTopologicalLattice` `instGroupOfIsTopologicalGroup` `Pi.instLattice` `Pi.group`	—	—
`instIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `ContinuousMap` `instAddCommMonoidOfContinuousAdd` `partialOrder`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`instIsOrderedMonoid` 📖	mathematical	—	`IsOrderedMonoid` `ContinuousMap` `instCommMonoidOfContinuousMul` `partialOrder`	—	`mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono`
`mabs_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `mabs` `instLatticeOfTopologicalLattice` `instGroupOfIsTopologicalGroup`	—	—

---