Bundled continuous maps into orders, with order-compatible topology #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
def
continuous_map.abs
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_ordered_add_comm_group β]
[order_topology β]
(f : C(α, β)) :
The pointwise absolute value of a continuous function as a continuous function.
@[protected, instance]
def
continuous_map.has_abs
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_ordered_add_comm_group β]
[order_topology β] :
@[simp]
theorem
continuous_map.abs_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_ordered_add_comm_group β]
[order_topology β]
(f : C(α, β))
(x : α) :
We now set up the partial order and lattice structure (given by pointwise min and max) on continuous functions.
@[protected, instance]
def
continuous_map.partial_order
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[partial_order β] :
Equations
- continuous_map.partial_order = partial_order.lift (λ (f : C(α, β)), f.to_fun) continuous_map.partial_order._proof_1
theorem
continuous_map.le_def
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[partial_order β]
{f g : C(α, β)} :
@[protected, instance]
def
continuous_map.has_sup
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_order β]
[order_closed_topology β] :
Equations
- continuous_map.has_sup = {sup := λ (f g : C(α, β)), {to_fun := λ (a : α), linear_order.max (⇑f a) (⇑g a), continuous_to_fun := _}}
@[simp, norm_cast]
theorem
continuous_map.sup_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_order β]
[order_closed_topology β]
(f g : C(α, β)) :
@[simp]
theorem
continuous_map.sup_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_order β]
[order_closed_topology β]
(f g : C(α, β))
(a : α) :
@[protected, instance]
def
continuous_map.semilattice_sup
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_order β]
[order_closed_topology β] :
Equations
- continuous_map.semilattice_sup = {sup := has_sup.sup continuous_map.has_sup, le := partial_order.le continuous_map.partial_order, lt := partial_order.lt continuous_map.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
@[protected, instance]
def
continuous_map.has_inf
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_order β]
[order_closed_topology β] :
Equations
- continuous_map.has_inf = {inf := λ (f g : C(α, β)), {to_fun := λ (a : α), linear_order.min (⇑f a) (⇑g a), continuous_to_fun := _}}
@[simp, norm_cast]
theorem
continuous_map.inf_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_order β]
[order_closed_topology β]
(f g : C(α, β)) :
@[simp]
theorem
continuous_map.inf_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_order β]
[order_closed_topology β]
(f g : C(α, β))
(a : α) :
@[protected, instance]
def
continuous_map.semilattice_inf
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_order β]
[order_closed_topology β] :
Equations
- continuous_map.semilattice_inf = {inf := has_inf.inf continuous_map.has_inf, le := partial_order.le continuous_map.partial_order, lt := partial_order.lt continuous_map.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
def
continuous_map.lattice
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_order β]
[order_closed_topology β] :
Equations
- continuous_map.lattice = {sup := semilattice_sup.sup continuous_map.semilattice_sup, le := semilattice_inf.le continuous_map.semilattice_inf, lt := semilattice_inf.lt continuous_map.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf continuous_map.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
theorem
continuous_map.sup'_apply
{β : Type u_2}
{γ : Type u_3}
[topological_space β]
[topological_space γ]
[linear_order γ]
[order_closed_topology γ]
{ι : Type u_1}
{s : finset ι}
(H : s.nonempty)
(f : ι → C(β, γ))
(b : β) :
@[simp, norm_cast]
theorem
continuous_map.sup'_coe
{β : Type u_2}
{γ : Type u_3}
[topological_space β]
[topological_space γ]
[linear_order γ]
[order_closed_topology γ]
{ι : Type u_1}
{s : finset ι}
(H : s.nonempty)
(f : ι → C(β, γ)) :
theorem
continuous_map.inf'_apply
{β : Type u_2}
{γ : Type u_3}
[topological_space β]
[topological_space γ]
[linear_order γ]
[order_closed_topology γ]
{ι : Type u_1}
{s : finset ι}
(H : s.nonempty)
(f : ι → C(β, γ))
(b : β) :
@[simp, norm_cast]
theorem
continuous_map.inf'_coe
{β : Type u_2}
{γ : Type u_3}
[topological_space β]
[topological_space γ]
[linear_order γ]
[order_closed_topology γ]
{ι : Type u_1}
{s : finset ι}
(H : s.nonempty)
(f : ι → C(β, γ)) :
def
continuous_map.Icc_extend
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_order α]
[order_topology α]
{a b : α}
(h : a ≤ b)
(f : C(↥(set.Icc a b), β)) :
Extend a continuous function f : C(set.Icc a b, β) to a function f : C(α, β).
Equations
- continuous_map.Icc_extend h f = {to_fun := set.Icc_extend h ⇑f, continuous_to_fun := _}
@[simp]
theorem
continuous_map.coe_Icc_extend
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[linear_order α]
[order_topology α]
{a b : α}
(h : a ≤ b)
(f : C(↥(set.Icc a b), β)) :
⇑(continuous_map.Icc_extend h f) = set.Icc_extend h ⇑f