Theorem Prod.mk_lt_mk_of_lt_of_le

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_lt_of_le View on Github →