mathlib3
44b81388 - chore(topology/instances/ennreal): use `tactic.lift` (#8788)

Commit
4 years ago
chore(topology/instances/ennreal): use `tactic.lift` (#8788) * use `tactic.lift` in two proofs; * use the `order_dual` trick in one proof.
Author
Parents
Loading