mathlib3
29036740 - refactor(order/conditionally_complete_lattice): tweak `well_founded.conditionally_complete_linear_order_with_bot` (#14706)

Commit
3 years ago
refactor(order/conditionally_complete_lattice): tweak `well_founded.conditionally_complete_linear_order_with_bot` (#14706) We change the `well_founded` assumption on `well_founded.conditionally_complete_linear_order_bot` to an equivalent but more convenient `is_well_order` typeclass assumption. As such, we place it in the `is_well_order` namespace.
Author
Parents
Loading