Documentation

Mathlib.Topology.ContinuousMap.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.

source
@[instance_reducible]
instance ContinuousMap.partialOrder {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [PartialOrder β] :
PartialOrder C(α, β)
source
theorem ContinuousMap.le_def {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [PartialOrder β] {f g : C(α, β)} :
f ≤ g ↔ ∀ (a : α), f a ≤ g a
source
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
source
@[instance_reducible]
instance ContinuousMap.sup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] :
Max C(α, β)
source
@[simp]
theorem ContinuousMap.coe_sup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] (f g : C(α, β)) :
⇑(f ⊔ g) = ⇑f ⊔ ⇑g
source
@[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
source
@[instance_reducible]
instance ContinuousMap.semilatticeSup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] :
SemilatticeSup C(α, β)
source
theorem ContinuousMap.sup'_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] {ι : Type u_3} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)) (a : α) :
(s.sup' H f) a = s.sup' H fun (i : ι) => (f i) a
source
@[simp]
theorem ContinuousMap.coe_sup' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeSup β] [ContinuousSup β] {ι : Type u_3} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)) :
⇑(s.sup' H f) = s.sup' H fun (i : ι) => ⇑(f i)
source
@[instance_reducible]
instance ContinuousMap.inf {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] :
Min C(α, β)
source
@[simp]
theorem ContinuousMap.coe_inf {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] (f g : C(α, β)) :
⇑(f ⊓ g) = ⇑f ⊓ ⇑g
source
@[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
source
@[instance_reducible]
instance ContinuousMap.semilatticeInf {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] :
SemilatticeInf C(α, β)
source
theorem ContinuousMap.inf'_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] {ι : Type u_3} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)) (a : α) :
(s.inf' H f) a = s.inf' H fun (i : ι) => (f i) a
source
@[simp]
theorem ContinuousMap.coe_inf' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SemilatticeInf β] [ContinuousInf β] {ι : Type u_3} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)) :
⇑(s.inf' H f) = s.inf' H fun (i : ι) => ⇑(f i)
source
@[instance_reducible]
instance ContinuousMap.instLatticeOfTopologicalLattice {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Lattice β] [TopologicalLattice β] :
Lattice C(α, β)
source
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(α, β).

Instances For
    source
    @[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), β)) :
    ⇑(IccExtend h f) = Set.IccExtend h ⇑f