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} [TopologicalSpace α] [TopologicalSpace β] [PartialOrder β] : PartialOrder C(α, β)

Equations

• ContinuousMap.partialOrder = PartialOrder.lift (fun (f : C(α, β)) => f.toFun) ⋯

theorem ContinuousMap.le_def {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [PartialOrder β] {f g : C(α, β)} : f ≤ g ↔ ∀ (a : α), f a ≤ g a

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

Equations

• ContinuousMap.sup = { max := 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 g : C(α, β)) : ⇑(f ⊔ g) = ⇑f ⊔ ⇑g

@[simp]

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

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

Equations

• ContinuousMap.semilatticeSup = Function.Injective.semilatticeSup (fun (f : C(α, β)) => ⇑f) ⋯ ⋯

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 : α) : (s.sup' H f) a = s.sup' 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(α, β)) : ⇑(s.sup' H f) = s.sup' H fun (i : ι) => ⇑(f i)

instance ContinuousMap.inf {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] : Min C(α, β)

Equations

• ContinuousMap.inf = { min := 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 g : C(α, β)) : ⇑(f ⊓ g) = ⇑f ⊓ ⇑g

@[simp]

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

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

Equations

• ContinuousMap.semilatticeInf = Function.Injective.semilatticeInf (fun (f : C(α, β)) => ⇑f) ⋯ ⋯

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 : α) : (s.inf' H f) a = s.inf' 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(α, β)) : ⇑(s.inf' H f) = s.inf' H fun (i : ι) => ⇑(f i)

instance ContinuousMap.instLatticeOfTopologicalLattice {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Lattice β] [TopologicalLattice β] : Lattice C(α, β)

Equations

• ContinuousMap.instLatticeOfTopologicalLattice = Function.Injective.lattice (fun (f : C(α, β)) => ⇑f) ⋯ ⋯ ⋯

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 = { toFun := Set.IccExtend h ⇑f, continuous_toFun := ⋯ }

@[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