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)] : C(↑(Set.Icc a b), ↑(Set.Icc a c))

The embedding into an interval from a sub-interval lying on the left, as a ContinuousMap.

Equations

• ContinuousMap.IccInclusionLeft = ContinuousMap.inclusion ⋯

def ContinuousMap.IccInclusionRight {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a b c : α} [Fact (a ≤ b)] : C(↑(Set.Icc b c), ↑(Set.Icc a c))

The embedding into an interval from a sub-interval lying on the right, as a ContinuousMap.

Equations

• ContinuousMap.IccInclusionRight = ContinuousMap.inclusion ⋯

def ContinuousMap.projIccCM {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {a b : α} [Fact (a ≤ b)] : C(α, ↑(Set.Icc 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] : C(C(↑(Set.Icc a b), E), C(α, 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) : (ContinuousMap.IccExtendCM f) x = f ⟨x, hx⟩

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)) : C(↑(Set.Icc a 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 ⊥) : (f.concat g).comp ContinuousMap.IccInclusionLeft = f

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 ⊥) : (f.concat g).comp ContinuousMap.IccInclusionRight = 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) : (f.concat g) t = f ⟨↑t, ⋯⟩

@[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) : (f.concat g) t = g ⟨↑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] : C({ fg : C(↑(Set.Icc a b), E) × C(↑(Set.Icc b c), E) // fg.1 ⊤ = fg.2 ⊥ }, C(↑(Set.Icc a c), E))

The concatenation of compatible pairs of continuous maps on adjacent intervals, defined as a ContinuousMap on a subtype of the product.

Equations

• ContinuousMap.concatCM = { toFun := fun (fg : { fg : C(↑(Set.Icc a b), E) × C(↑(Set.Icc b c), E) // fg.1 ⊤ = fg.2 ⊥ }) => (↑fg).1.concat (↑fg).2, continuous_toFun := ⋯ }

@[simp]

theorem ContinuousMap.concatCM_left {α : 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 : ↑x ≤ b) {fg : { fg : C(↑(Set.Icc a b), E) × C(↑(Set.Icc b c), E) // fg.1 ⊤ = fg.2 ⊥ }} : (ContinuousMap.concatCM fg) x = (↑fg).1 ⟨↑x, ⋯⟩

@[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 ⊥ }} : (ContinuousMap.concatCM fg) x = (↑fg).2 ⟨↑x, ⋯⟩