Theorem Prod.mk_lt_mk_of_le_of_lt

Modification history

2024-06-17 10:24

Mathlib/Order/Basic.lean

feat: `(𝓝[<] x).NeBot` instances for `Prod`, `Pi`, `OrderDual` (#13642)

Added Prod.mk_lt_mk_of_le_of_lt View on Github →