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.

theorem continuous_at_sign_of_ne_zero {α : Type u_1} [has_zero α] [topological_space α] [linear_order α] [order_topology α] {a : α} (h : a 0) :