# Documentation

Mathlib.Topology.ContinuousFunction.Ordered

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

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

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

Instances For
instance ContinuousMap.instAbsContinuousMap {α : Type u_1} {β : Type u_2} [] [] [] :
Abs C(α, β)
@[simp]
theorem ContinuousMap.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.

instance ContinuousMap.partialOrder {α : Type u_1} {β : Type u_2} [] [] [] :
theorem ContinuousMap.le_def {α : Type u_1} {β : Type u_2} [] [] [] {f : C(α, β)} {g : C(α, β)} :
f g ∀ (a : α), f a g a
theorem ContinuousMap.lt_def {α : Type u_1} {β : Type u_2} [] [] [] {f : C(α, β)} {g : C(α, β)} :
f < g (∀ (a : α), f a g a) a, f a < g a
instance ContinuousMap.sup {α : Type u_1} {β : Type u_2} [] [] [] :
Sup C(α, β)
@[simp]
theorem ContinuousMap.sup_coe {α : Type u_1} {β : Type u_2} [] [] [] (f : C(α, β)) (g : C(α, β)) :
↑(f g) = f g
@[simp]
theorem ContinuousMap.sup_apply {α : Type u_1} {β : Type u_2} [] [] [] (f : C(α, β)) (g : C(α, β)) (a : α) :
↑(f g) a = max (f a) (g a)
instance ContinuousMap.semilatticeSup {α : Type u_1} {β : Type u_2} [] [] [] :
instance ContinuousMap.inf {α : Type u_1} {β : Type u_2} [] [] [] :
Inf C(α, β)
@[simp]
theorem ContinuousMap.inf_coe {α : Type u_1} {β : Type u_2} [] [] [] (f : C(α, β)) (g : C(α, β)) :
↑(f g) = f g
@[simp]
theorem ContinuousMap.inf_apply {α : Type u_1} {β : Type u_2} [] [] [] (f : C(α, β)) (g : C(α, β)) (a : α) :
↑(f g) a = min (f a) (g a)
instance ContinuousMap.semilatticeInf {α : Type u_1} {β : Type u_2} [] [] [] :
instance ContinuousMap.instLatticeContinuousMap {α : Type u_1} {β : Type u_2} [] [] [] :
theorem ContinuousMap.sup'_apply {β : Type u_2} {γ : Type u_3} [] [] [] {ι : Type u_4} {s : } (H : ) (f : ιC(β, γ)) (b : β) :
↑(Finset.sup' s H f) b = Finset.sup' s H fun a => ↑(f a) b
@[simp]
theorem ContinuousMap.sup'_coe {β : Type u_2} {γ : Type u_3} [] [] [] {ι : Type u_4} {s : } (H : ) (f : ιC(β, γ)) :
↑(Finset.sup' s H f) = Finset.sup' s H fun a => ↑(f a)
theorem ContinuousMap.inf'_apply {β : Type u_2} {γ : Type u_3} [] [] [] {ι : Type u_4} {s : } (H : ) (f : ιC(β, γ)) (b : β) :
↑(Finset.inf' s H f) b = Finset.inf' s H fun a => ↑(f a) b
@[simp]
theorem ContinuousMap.inf'_coe {β : Type u_2} {γ : Type u_3} [] [] [] {ι : Type u_4} {s : } (H : ) (f : ιC(β, γ)) :
↑(Finset.inf' s H f) = Finset.inf' s H fun a => ↑(f a)
def ContinuousMap.IccExtend {α : Type u_1} {β : Type u_2} [] [] [] [] {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(α, β).

Instances For
@[simp]
theorem ContinuousMap.coe_IccExtend {α : Type u_1} {β : Type u_2} [] [] [] [] {a : α} {b : α} (h : a b) (f : C(↑(Set.Icc a b), β)) :
↑() =