mathlib3

1cdd8266 - feat(topology/instances/sign): topology of `sign_type` and `sign` (#15925)

feat(topology/instances/sign): topology of `sign_type` and `sign` (#15925) Give `sign_type` the discrete topology, and prove that `sign`, in an `order_topology`, is continuous at positive and negative arguments (in a `partial_order`) or away from zero (in a `linear_order`).