Continuous bundled maps on intervals #
In this file we prove a few results about ContinuousMap when the domain is an interval.
def
ContinuousMap.IccInclusionLeft
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
{a b c : α}
[Fact (b ≤ c)]
:
The embedding into an interval from a sub-interval lying on the left, as a ContinuousMap.
def
ContinuousMap.IccInclusionRight
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
{a b c : α}
[Fact (a ≤ b)]
:
The embedding into an interval from a sub-interval lying on the right, as a ContinuousMap.
def
ContinuousMap.projIccCM
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{a b : α}
[Fact (a ≤ b)]
:
The map projIcc from α onto an interval in α, as a ContinuousMap.
Equations
- ContinuousMap.projIccCM = { toFun := Set.projIcc a b ⋯, continuous_toFun := ⋯ }
def
ContinuousMap.IccExtendCM
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{a b : α}
[Fact (a ≤ b)]
{E : Type u_2}
[TopologicalSpace E]
:
The extension operation from continuous maps on an interval to continuous maps on the whole
type, as a ContinuousMap.
Equations
- ContinuousMap.IccExtendCM = { toFun := fun (f : C(↑(Set.Icc a b), E)) => f.comp ContinuousMap.projIccCM, continuous_toFun := ⋯ }
@[simp]
theorem
ContinuousMap.IccExtendCM_of_mem
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{a b : α}
[Fact (a ≤ b)]
{E : Type u_2}
[TopologicalSpace E]
{f : C(↑(Set.Icc a b), E)}
{x : α}
(hx : x ∈ Set.Icc a b)
:
noncomputable def
ContinuousMap.concat
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{a b c : α}
[Fact (a ≤ b)]
[Fact (b ≤ c)]
{E : Type u_2}
[TopologicalSpace E]
(f : C(↑(Set.Icc a b), E))
(g : C(↑(Set.Icc b c), E))
:
The concatenation of two continuous maps defined on adjacent intervals. If the values of the
functions on the common bound do not agree, this is defined as an arbitrarily chosen constant
map. See concatCM for the corresponding map on the subtype of compatible function pairs.
Equations
- One or more equations did not get rendered due to their size.
theorem
ContinuousMap.concat_comp_IccInclusionLeft
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{a b c : α}
[Fact (a ≤ b)]
[Fact (b ≤ c)]
{E : Type u_2}
[TopologicalSpace E]
{f : C(↑(Set.Icc a b), E)}
{g : C(↑(Set.Icc b c), E)}
(hb : f ⊤ = g ⊥)
:
theorem
ContinuousMap.concat_comp_IccInclusionRight
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{a b c : α}
[Fact (a ≤ b)]
[Fact (b ≤ c)]
{E : Type u_2}
[TopologicalSpace E]
{f : C(↑(Set.Icc a b), E)}
{g : C(↑(Set.Icc b c), E)}
(hb : f ⊤ = g ⊥)
:
@[simp]
theorem
ContinuousMap.concat_left
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{a b c : α}
[Fact (a ≤ b)]
[Fact (b ≤ c)]
{E : Type u_2}
[TopologicalSpace E]
{f : C(↑(Set.Icc a b), E)}
{g : C(↑(Set.Icc b c), E)}
(hb : f ⊤ = g ⊥)
{t : ↑(Set.Icc a c)}
(ht : ↑t ≤ b)
:
@[simp]
theorem
ContinuousMap.concat_right
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{a b c : α}
[Fact (a ≤ b)]
[Fact (b ≤ c)]
{E : Type u_2}
[TopologicalSpace E]
{f : C(↑(Set.Icc a b), E)}
{g : C(↑(Set.Icc b c), E)}
(hb : f ⊤ = g ⊥)
{t : ↑(Set.Icc a c)}
(ht : b ≤ ↑t)
:
theorem
ContinuousMap.tendsto_concat
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{a b c : α}
[Fact (a ≤ b)]
[Fact (b ≤ c)]
{E : Type u_2}
[TopologicalSpace E]
{f : C(↑(Set.Icc a b), E)}
{g : C(↑(Set.Icc b c), E)}
{ι : Type u_3}
{p : Filter ι}
{F : ι → C(↑(Set.Icc a b), E)}
{G : ι → C(↑(Set.Icc b c), E)}
(hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥)
(hfg' : f ⊤ = g ⊥)
(hf : Filter.Tendsto F p (nhds f))
(hg : Filter.Tendsto G p (nhds g))
:
Filter.Tendsto (fun (i : ι) => (F i).concat (G i)) p (nhds (f.concat g))
noncomputable def
ContinuousMap.concatCM
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{a b c : α}
[Fact (a ≤ b)]
[Fact (b ≤ c)]
{E : Type u_2}
[TopologicalSpace E]
:
The concatenation of compatible pairs of continuous maps on adjacent intervals, defined as a
ContinuousMap on a subtype of the product.
@[simp]
@[simp]
theorem
ContinuousMap.concatCM_right
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{a b c : α}
[Fact (a ≤ b)]
[Fact (b ≤ c)]
{E : Type u_2}
[TopologicalSpace E]
{x : ↑(Set.Icc a c)}
(hx : b ≤ ↑x)
{fg : { fg : C(↑(Set.Icc a b), E) × C(↑(Set.Icc b c), E) // fg.1 ⊤ = fg.2 ⊥ }}
: