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 (since := "2024-09-12")]
theorem max_commutative {α : Type u} [LinearOrder α] :
Commutative max
source
@[deprecated instAssociativeMax (since := "2024-09-12")]
theorem max_associative {α : Type u} [LinearOrder α] :
Associative max
source
@[deprecated instCommutativeMin (since := "2024-09-12")]
theorem min_commutative {α : Type u} [LinearOrder α] :
Commutative min
source
@[deprecated instAssociativeMin (since := "2024-09-12")]
theorem min_associative {α : Type u} [LinearOrder α] :
Associative min