Mathlib.Topology.Order.ProjIcc

Filter.Tendsto.IccExtend theorem

 (f : γ → Icc a b → β) {la : Filter α} {lb : Filter β} {lc : Filter γ}
  (hf : Tendsto (↿f) (lc ×ˢ la.map (projIcc a b h)) lb) : Tendsto (↿(IccExtend h ∘ f)) (lc ×ˢ la) lb

Full source

protected theorem Filter.Tendsto.IccExtend (f : γ → Icc a b → β) {la : Filter α} {lb : Filter β}
    {lc : Filter γ} (hf : Tendsto (↿f) (lc ×ˢ la.map (projIcc a b h)) lb) :
    Tendsto (↿(IccExtend h ∘ f)) (lc ×ˢ la) lb :=
  hf.comp <| tendsto_id.prodMap tendsto_map

Tendsto Property of Extended Function via Projection onto Closed Interval

Informal description

Let $f : \gamma \to [a, b] \to \beta$ be a function, where $[a, b]$ is a closed interval in a linearly ordered type $\alpha$ with $a \leq b$. Given filters $l_a$ on $\alpha$, $l_b$ on $\beta$, and $l_c$ on $\gamma$, if the uncurried function $\uncurry f$ tends to $l_b$ along the product filter $l_c \times l_a'$, where $l_a'$ is the pushforward of $l_a$ under the projection $\text{projIcc}(a, b, h)$, then the uncurried function $\uncurry (\text{IccExtend}(h) \circ f)$ tends to $l_b$ along the product filter $l_c \times l_a$.

continuous_projIcc theorem

: Continuous (projIcc a b h)

Full source

@[continuity]
theorem continuous_projIcc : Continuous (projIcc a b h) :=
  (continuous_const.max <| continuous_const.min continuous_id).subtype_mk _

Continuity of Projection onto Closed Interval $[a, b]$

Informal description

The projection function $\text{projIcc}(a, b, h) \colon \alpha \to [a, b]$ is continuous, where $[a, b]$ is a closed interval in a linearly ordered type $\alpha$ and $h$ is a proof that $a \leq b$.

isQuotientMap_projIcc theorem

: IsQuotientMap (projIcc a b h)

Full source

theorem isQuotientMap_projIcc : IsQuotientMap (projIcc a b h) :=
  isQuotientMap_iff.2 ⟨projIcc_surjective h, fun s =>
    ⟨fun hs => hs.preimage continuous_projIcc, fun hs => ⟨_, hs, by ext; simp⟩⟩⟩

Projection onto Closed Interval is a Quotient Map

Informal description

The projection function $\text{projIcc}_{a,b} \colon \alpha \to [a, b]$ is a quotient map, where $[a, b]$ is a closed interval in a linearly ordered type $\alpha$ and $h$ is a proof that $a \leq b$.

continuous_IccExtend_iff theorem

{f : Icc a b → β} : Continuous (IccExtend h f) ↔ Continuous f

Full source

@[simp]
theorem continuous_IccExtend_iff {f : Icc a b → β} : ContinuousContinuous (IccExtend h f) ↔ Continuous f :=
  isQuotientMap_projIcc.continuous_iff.symm

Continuity of Extended Function via Interval Projection if and only if Original Function is Continuous

Informal description

Let $[a, b]$ be a closed interval in a linearly ordered type $\alpha$ with $a \leq b$, and let $f \colon [a, b] \to \beta$ be a function. The extension $\text{IccExtend}(h, f) \colon \alpha \to \beta$ is continuous if and only if $f$ is continuous.

Continuous.IccExtend theorem

 {f : γ → Icc a b → β} {g : γ → α} (hf : Continuous ↿f) (hg : Continuous g) :
  Continuous fun a => IccExtend h (f a) (g a)

Full source

/-- See Note [continuity lemma statement]. -/
protected theorem Continuous.IccExtend {f : γ → Icc a b → β} {g : γ → α} (hf : Continuous ↿f)
    (hg : Continuous g) : Continuous fun a => IccExtend h (f a) (g a) :=
  show Continuous (↿f↿f ∘ fun x => (x, projIcc a b h (g x)))
  from hf.comp <| continuous_id.prodMk <| continuous_projIcc.comp hg

Continuity of Extended Function via Interval Projection

Informal description

Let $\gamma$ and $\beta$ be topological spaces, and let $[a, b]$ be a closed interval in a linearly ordered type $\alpha$ with $a \leq b$. Given a continuous function $f \colon \gamma \to [a, b] \to \beta$ and a continuous function $g \colon \gamma \to \alpha$, the extended function $a \mapsto \text{IccExtend}(h, f(a))(g(a))$ is continuous, where $\text{IccExtend}(h, \cdot)$ extends a function defined on $[a, b]$ to all of $\alpha$ via projection onto $[a, b]$.

Continuous.Icc_extend' theorem

{f : Icc a b → β} (hf : Continuous f) : Continuous (IccExtend h f)

Full source

/-- A useful special case of `Continuous.IccExtend`. -/
@[continuity]
protected theorem Continuous.Icc_extend' {f : Icc a b → β} (hf : Continuous f) :
    Continuous (IccExtend h f) :=
  hf.comp continuous_projIcc

Continuity of the Extension from a Closed Interval

Informal description

For any continuous function $f \colon [a, b] \to \beta$ defined on a closed interval $[a, b]$ in a linearly ordered type $\alpha$ (where $h$ is a proof that $a \leq b$), the extended function $\text{IccExtend}(h, f) \colon \alpha \to \beta$ is also continuous.

ContinuousAt.IccExtend theorem

 {x : γ} (f : γ → Icc a b → β) {g : γ → α} (hf : ContinuousAt (↿f) (x, projIcc a b h (g x))) (hg : ContinuousAt g x) :
  ContinuousAt (fun a => IccExtend h (f a) (g a)) x

Full source

theorem ContinuousAt.IccExtend {x : γ} (f : γ → Icc a b → β) {g : γ → α}
    (hf : ContinuousAt (↿f) (x, projIcc a b h (g x))) (hg : ContinuousAt g x) :
    ContinuousAt (fun a => IccExtend h (f a) (g a)) x :=
  show ContinuousAt (↿f↿f ∘ fun x => (x, projIcc a b h (g x))) x from
    ContinuousAt.comp hf <| continuousAt_id.prodMk <| continuous_projIcc.continuousAt.comp hg

Continuity of Interval Extension at a Point

Informal description

Let $\gamma$ and $\alpha$ be topological spaces, and let $[a, b]$ be a closed interval in $\alpha$ with $a \leq b$. Given a function $f \colon \gamma \times [a, b] \to \beta$ that is continuous at $(x, \text{projIcc}(a, b, h)(g(x)))$ and a function $g \colon \gamma \to \alpha$ that is continuous at $x$, the extended function $\gamma \to \beta$ defined by $a \mapsto \text{IccExtend}(h, f(a))(g(a))$ is continuous at $x$.