Documentation

Mathlib.Topology.ContinuousFunction.Ordered

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.

Equations
theorem ContinuousMap.le_def {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [PartialOrder β] {f : C(α, β)} {g : C(α, β)} :
f g ∀ (a : α), f a g a
theorem ContinuousMap.lt_def {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [PartialOrder β] {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} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] :
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} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f : C(α, β)) (g : C(α, β)) :
(f g) = f g
@[simp]
theorem ContinuousMap.sup_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f : C(α, β)) (g : C(α, β)) (a : α) :
(f g) a = f a g a
Equations
theorem ContinuousMap.sup'_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] {ι : Type u_4} {s : Finset ι} (H : s.Nonempty) (f : ιC(α, β)) (a : α) :
(Finset.sup' s H f) a = Finset.sup' s H fun (i : ι) => (f i) a
@[simp]
theorem ContinuousMap.coe_sup' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] {ι : Type u_4} {s : Finset ι} (H : s.Nonempty) (f : ιC(α, β)) :
(Finset.sup' s H f) = Finset.sup' s H fun (i : ι) => (f i)
instance ContinuousMap.inf {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] :
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} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f : C(α, β)) (g : C(α, β)) :
(f g) = f g
@[simp]
theorem ContinuousMap.inf_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f : C(α, β)) (g : C(α, β)) (a : α) :
(f g) a = f a g a
Equations
theorem ContinuousMap.inf'_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] {ι : Type u_4} {s : Finset ι} (H : s.Nonempty) (f : ιC(α, β)) (a : α) :
(Finset.inf' s H f) a = Finset.inf' s H fun (i : ι) => (f i) a
@[simp]
theorem ContinuousMap.coe_inf' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] {ι : Type u_4} {s : Finset ι} (H : s.Nonempty) (f : ιC(α, β)) :
(Finset.inf' s H f) = Finset.inf' s H fun (i : ι) => (f i)
Equations
def ContinuousMap.IccExtend {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrder α] [OrderTopology α] {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
Instances For
    @[simp]
    theorem ContinuousMap.coe_IccExtend {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (h : a b) (f : C((Set.Icc a b), β)) :