mathlib documentation

topology.continuous_function.ordered

Bundled continuous maps into orders, with order-compatible topology #

def continuous_map.abs {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_ordered_add_comm_group β] [order_topology β] (f : C(α, β)) :
C(α, β)

The pointwise absolute value of a continuous function as a continuous function.

Equations
@[protected, instance]
Equations
@[simp]
theorem continuous_map.abs_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_ordered_add_comm_group β] [order_topology β] (f : C(α, β)) (x : α) :
|f| x = |f x|

We now set up the partial order and lattice structure (given by pointwise min and max) on continuous functions.

@[protected, instance]
def continuous_map.partial_order {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [partial_order β] :
Equations
theorem continuous_map.le_def {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [partial_order β] {f g : C(α, β)} :
f g ∀ (a : α), f a g a
theorem continuous_map.lt_def {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [partial_order β] {f g : C(α, β)} :
f < g (∀ (a : α), f a g a) ∃ (a : α), f a < g a
@[protected, instance]
def continuous_map.has_sup {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] :
Equations
@[simp, norm_cast]
theorem continuous_map.sup_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] (f g : C(α, β)) :
(f g) = f g
@[simp]
theorem continuous_map.sup_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] (f g : C(α, β)) (a : α) :
(f g) a = linear_order.max (f a) (g a)
@[protected, instance]
def continuous_map.has_inf {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] :
Equations
@[simp, norm_cast]
theorem continuous_map.inf_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] (f g : C(α, β)) :
(f g) = f g
@[simp]
theorem continuous_map.inf_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order β] [order_closed_topology β] (f g : C(α, β)) (a : α) :
(f g) a = linear_order.min (f a) (g a)
theorem continuous_map.sup'_apply {β : Type u_2} {γ : Type u_3} [topological_space β] [topological_space γ] [linear_order γ] [order_closed_topology γ] {ι : Type u_1} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) (b : β) :
(s.sup' H f) b = s.sup' H (λ (a : ι), (f a) b)
@[simp, norm_cast]
theorem continuous_map.sup'_coe {β : Type u_2} {γ : Type u_3} [topological_space β] [topological_space γ] [linear_order γ] [order_closed_topology γ] {ι : Type u_1} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) :
(s.sup' H f) = s.sup' H (λ (a : ι), (f a))
theorem continuous_map.inf'_apply {β : Type u_2} {γ : Type u_3} [topological_space β] [topological_space γ] [linear_order γ] [order_closed_topology γ] {ι : Type u_1} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) (b : β) :
(s.inf' H f) b = s.inf' H (λ (a : ι), (f a) b)
@[simp, norm_cast]
theorem continuous_map.inf'_coe {β : Type u_2} {γ : Type u_3} [topological_space β] [topological_space γ] [linear_order γ] [order_closed_topology γ] {ι : Type u_1} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) :
(s.inf' H f) = s.inf' H (λ (a : ι), (f a))
def continuous_map.Icc_extend {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order α] [order_topology α] {a b : α} (h : a b) (f : C((set.Icc a b), β)) :
C(α, β)

Extend a continuous function f : C(set.Icc a b, β) to a function f : C(α, β).

Equations
@[simp]
theorem continuous_map.coe_Icc_extend {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [linear_order α] [order_topology α] {a b : α} (h : a b) (f : C((set.Icc a b), β)) :