Documentation

Mathlib.Deprecated.MinMax

Note about deprecated files #

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

source
@[deprecated instCommutativeMax]
theorem max_commutative {α : Type u} [LinearOrder α] :
Commutative max
source
@[deprecated instAssociativeMax]
theorem max_associative {α : Type u} [LinearOrder α] :
Associative max
source
@[deprecated instCommutativeMin]
theorem min_commutative {α : Type u} [LinearOrder α] :
Commutative min
source
@[deprecated instAssociativeMin]
theorem min_associative {α : Type u} [LinearOrder α] :
Associative min