Documentation

Mathlib.Topology.EMetricSpace.MulOpposite

Extended metric spaces on multiplicative opposites #

This file proves that if α is some (weak) pseudo extended metric space, so is αᵐᵒᵖ. We do this in this file instead of Mathlib/Topology/EMetricSpace/Defs.lean to avoid imports.

source
@[instance_reducible]
instance MulOpposite.instWeakPseudoEMetricSpace {α : Type u_2} [TopologicalSpace α] [WeakPseudoEMetricSpace α] :
WeakPseudoEMetricSpace αᵐᵒᵖ

weak pseudoemetric space instance on the multiplicative opposite of a weak pseudoemetric space.

Equations
source
@[instance_reducible]
instance AddOpposite.instWeakPseudoEMetricSpace {α : Type u_2} [TopologicalSpace α] [WeakPseudoEMetricSpace α] :
WeakPseudoEMetricSpace αᵃᵒᵖ

Weak pseudoemetric space instance on the additive opposite of a weak pseudoemetric space.

Equations
source
@[instance_reducible]
instance MulOpposite.instPseudoEMetricSpace {α : Type u_2} [PseudoEMetricSpace α] :
PseudoEMetricSpace αᵐᵒᵖ

Pseudoemetric space instance on the multiplicative opposite of a pseudoemetric space.

Equations
source
@[instance_reducible]
instance AddOpposite.instPseudoEMetricSpace {α : Type u_2} [PseudoEMetricSpace α] :
PseudoEMetricSpace αᵃᵒᵖ

Pseudoemetric space instance on the additive opposite of a pseudoemetric space.

Equations
source
theorem MulOpposite.edist_unop {α : Type u_1} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y : αᵐᵒᵖ) :
edist (unop x) (unop y) = edist x y
source
theorem AddOpposite.edist_unop {α : Type u_1} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y : αᵃᵒᵖ) :
edist (unop x) (unop y) = edist x y
source
theorem MulOpposite.edist_op {α : Type u_1} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y : α) :
edist (op x) (op y) = edist x y
source
theorem AddOpposite.edist_op {α : Type u_1} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y : α) :
edist (op x) (op y) = edist x y