Bundled continuous maps into orders, with order-compatible topology

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

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

Equations

• ContinuousMap.abs f = ContinuousMap.mk fun x => |↑f x|

instance ContinuousMap.instAbsContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrderedAddCommGroup β] [OrderTopology β] : Abs C(α, β)

Equations

• ContinuousMap.instAbsContinuousMap = { abs := fun f => ContinuousMap.abs f }

@[simp]

theorem ContinuousMap.abs_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrderedAddCommGroup β] [OrderTopology β] (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} [TopologicalSpace α] [TopologicalSpace β] [PartialOrder β] : PartialOrder C(α, β)

Equations

• ContinuousMap.partialOrder = PartialOrder.lift (fun f => f.toFun) (_ : ∀ (f g : C(α, β)), (fun f => f.toFun) f = (fun f => f.toFun) g → f = g)

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 β] [LinearOrder β] [OrderClosedTopology β] : Sup C(α, β)

Equations

• ContinuousMap.sup = { sup := fun f g => ContinuousMap.mk fun a => max (↑f a) (↑g a) }

@[simp]

theorem ContinuousMap.sup_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] (f : C(α, β)) (g : C(α, β)) : ↑(f ⊔ g) = ↑f ⊔ ↑g

@[simp]

theorem ContinuousMap.sup_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] (f : C(α, β)) (g : C(α, β)) (a : α) : ↑(f ⊔ g) a = max (↑f a) (↑g a)

instance ContinuousMap.semilatticeSup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] : SemilatticeSup C(α, β)

Equations

• One or more equations did not get rendered due to their size.

instance ContinuousMap.inf {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] : Inf C(α, β)

Equations

• ContinuousMap.inf = { inf := fun f g => ContinuousMap.mk fun a => min (↑f a) (↑g a) }

@[simp]

theorem ContinuousMap.inf_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] (f : C(α, β)) (g : C(α, β)) : ↑(f ⊓ g) = ↑f ⊓ ↑g

@[simp]

theorem ContinuousMap.inf_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] (f : C(α, β)) (g : C(α, β)) (a : α) : ↑(f ⊓ g) a = min (↑f a) (↑g a)

instance ContinuousMap.semilatticeInf {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] : SemilatticeInf C(α, β)

Equations

• One or more equations did not get rendered due to their size.

instance ContinuousMap.instLatticeContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] : Lattice C(α, β)

Equations

• One or more equations did not get rendered due to their size.

theorem ContinuousMap.sup'_apply {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] [TopologicalSpace γ] [LinearOrder γ] [OrderClosedTopology γ] {ι : Type u_4} {s : Finset ι} (H : Finset.Nonempty s) (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} [TopologicalSpace β] [TopologicalSpace γ] [LinearOrder γ] [OrderClosedTopology γ] {ι : Type u_4} {s : Finset ι} (H : Finset.Nonempty s) (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} [TopologicalSpace β] [TopologicalSpace γ] [LinearOrder γ] [OrderClosedTopology γ] {ι : Type u_4} {s : Finset ι} (H : Finset.Nonempty s) (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} [TopologicalSpace β] [TopologicalSpace γ] [LinearOrder γ] [OrderClosedTopology γ] {ι : Type u_4} {s : Finset ι} (H : Finset.Nonempty s) (f : ι → C(β, γ)) : ↑(Finset.inf' s H f) = Finset.inf' s H fun a => ↑(f a)

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

• ContinuousMap.IccExtend h f = ContinuousMap.mk (Set.IccExtend h ↑f)

@[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), β)) : ↑(ContinuousMap.IccExtend h f) = Set.IccExtend h ↑f