mathlib documentation

topology.instances.sign

Topology on sign_type #

This file gives sign_type the discrete topology, and proves continuity results for sign in an order_topology.