mathlib3 documentation

topology.instances.sign

Topology on sign_type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[protected, instance]
def sign_type.topological_space  :
topological_space sign_type
Equations
source
@[protected, instance]
def sign_type.discrete_topology  :
discrete_topology sign_type
source
theorem continuous_at_sign_of_pos {α : Type u_1} [has_zero α] [topological_space α] [partial_order α] [decidable_rel has_lt.lt] [order_topology α] {a : α} (h : 0 < a) :
continuous_at ⇑sign a
source
theorem continuous_at_sign_of_neg {α : Type u_1} [has_zero α] [topological_space α] [partial_order α] [decidable_rel has_lt.lt] [order_topology α] {a : α} (h : a < 0) :
continuous_at ⇑sign a
source
theorem continuous_at_sign_of_ne_zero {α : Type u_1} [has_zero α] [topological_space α] [linear_order α] [order_topology α] {a : α} (h : a ≠ 0) :
continuous_at ⇑sign a