# mathlibdocumentation

topology.continuous_function.ordered

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

def continuous_map.abs {α : Type u_1} {β : Type u_2} (f : C(α, β)) :
C(α, β)

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

Equations
@[protected, instance]
def continuous_map.has_abs {α : Type u_1} {β : Type u_2}  :
Equations
@[simp]
theorem continuous_map.abs_apply {α : Type u_1} {β : Type u_2} (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}  :
Equations
theorem continuous_map.le_def {α : Type u_1} {β : Type u_2} {f g : C(α, β)} :
f g ∀ (a : α), f a g a
theorem continuous_map.lt_def {α : Type u_1} {β : Type u_2} {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} [linear_order β]  :
Equations
@[simp, norm_cast]
theorem continuous_map.sup_coe {α : Type u_1} {β : Type u_2} [linear_order β] (f g : C(α, β)) :
(f g) = f g
@[simp]
theorem continuous_map.sup_apply {α : Type u_1} {β : Type u_2} [linear_order β] (f g : C(α, β)) (a : α) :
(f g) a = linear_order.max (f a) (g a)
@[protected, instance]
def continuous_map.semilattice_sup {α : Type u_1} {β : Type u_2} [linear_order β]  :
Equations
@[protected, instance]
def continuous_map.has_inf {α : Type u_1} {β : Type u_2} [linear_order β]  :
Equations
@[simp, norm_cast]
theorem continuous_map.inf_coe {α : Type u_1} {β : Type u_2} [linear_order β] (f g : C(α, β)) :
(f g) = f g
@[simp]
theorem continuous_map.inf_apply {α : Type u_1} {β : Type u_2} [linear_order β] (f g : C(α, β)) (a : α) :
(f g) a = linear_order.min (f a) (g a)
@[protected, instance]
def continuous_map.semilattice_inf {α : Type u_1} {β : Type u_2} [linear_order β]  :
Equations
@[protected, instance]
def continuous_map.lattice {α : Type u_1} {β : Type u_2} [linear_order β]  :
Equations
theorem continuous_map.sup'_apply {β : Type u_2} {γ : Type u_3} [linear_order γ] {ι : 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} [linear_order γ] {ι : 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} [linear_order γ] {ι : 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} [linear_order γ] {ι : 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} [linear_order α] {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} [linear_order α] {a b : α} (h : a b) (f : C((set.Icc a b), β)) :