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

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} [] [] [] :
Equations
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(α, β)
Equations
• ContinuousMap.sup = { sup := fun (f g : C(α, β)) => { toFun := fun (a : α) => f a g a, continuous_toFun := } }
@[simp]
theorem ContinuousMap.coe_sup {α : 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 = f a g a
instance ContinuousMap.semilatticeSup {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
theorem ContinuousMap.sup'_apply {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_4} {s : } (H : s.Nonempty) (f : ιC(α, β)) (a : α) :
(s.sup' H f) a = s.sup' H fun (i : ι) => (f i) a
@[simp]
theorem ContinuousMap.coe_sup' {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_4} {s : } (H : s.Nonempty) (f : ιC(α, β)) :
(s.sup' H f) = s.sup' H fun (i : ι) => (f i)
instance ContinuousMap.inf {α : Type u_1} {β : Type u_2} [] [] [] [] :
Inf C(α, β)
Equations
• ContinuousMap.inf = { inf := fun (f g : C(α, β)) => { toFun := fun (a : α) => f a g a, continuous_toFun := } }
@[simp]
theorem ContinuousMap.coe_inf {α : 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 = f a g a
instance ContinuousMap.semilatticeInf {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
theorem ContinuousMap.inf'_apply {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_4} {s : } (H : s.Nonempty) (f : ιC(α, β)) (a : α) :
(s.inf' H f) a = s.inf' H fun (i : ι) => (f i) a
@[simp]
theorem ContinuousMap.coe_inf' {α : Type u_1} {β : Type u_2} [] [] [] [] {ι : Type u_4} {s : } (H : s.Nonempty) (f : ιC(α, β)) :
(s.inf' H f) = s.inf' H fun (i : ι) => (f i)
instance ContinuousMap.instLatticeOfTopologicalLattice {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
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(α, β).

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