Càdlàg functions

This file defines càdlàg functions, i.e. right-continuous functions with left limits. These are for instance a common hypothesis made on stochastic processes.

Using the to_dual machinery we also define càglàd functions (left-continuous with right limits).

def IsRightContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Preorder X] [TopologicalSpace Y] (f : X → Y) : Prop

A function f is right-continuous if for any a, f x → f a when x → a and x > a.

Equations

• IsRightContinuous f = ∀ (a : X), ContinuousWithinAt f (Set.Ioi a) a

def IsLeftContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Preorder X] [TopologicalSpace Y] (f : X → Y) : Prop

A function f is left-continuous if for any a, f x → f a when x → a and x < a.

Equations

• IsLeftContinuous f = ∀ (a : X), ContinuousWithinAt f (Set.Iio a) a

theorem Continuous.isRightContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] (hf : Continuous f) : IsRightContinuous f

theorem Continuous.isLeftContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] (hf : Continuous f) : IsLeftContinuous f

theorem IsRightContinuous.continuous_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] {g : Y → Z} (hf : IsRightContinuous f) (hg : Continuous g) : IsRightContinuous (g ∘ f)

theorem IsLeftContinuous.continuous_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] {g : Y → Z} (hf : IsLeftContinuous f) (hg : Continuous g) : IsLeftContinuous (g ∘ f)

theorem IsLeftContinuous.fun_continuous_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] {g : Y → Z} (hf : IsLeftContinuous f) (hg : Continuous g) : IsLeftContinuous fun (x : X) => g (f x)

Eta-expanded form of IsLeftContinuous.continuous_comp

theorem IsRightContinuous.fun_continuous_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] {g : Y → Z} (hf : IsRightContinuous f) (hg : Continuous g) : IsRightContinuous fun (x : X) => g (f x)

Eta-expanded form of IsRightContinuous.continuous_comp

theorem IsRightContinuous.continuous_comp₂ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} {T : Type u_4} [TopologicalSpace Z] [TopologicalSpace T] {g : X → Z} {φ : Y → Z → T} (hf : IsRightContinuous f) (hg : IsRightContinuous g) (hφ : Continuous (Function.uncurry φ)) : IsRightContinuous fun (x : X) => φ (f x) (g x)

theorem IsLeftContinuous.continuous_comp₂ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} {T : Type u_4} [TopologicalSpace Z] [TopologicalSpace T] {g : X → Z} {φ : Y → Z → T} (hf : IsLeftContinuous f) (hg : IsLeftContinuous g) (hφ : Continuous (Function.uncurry φ)) : IsLeftContinuous fun (x : X) => φ (f x) (g x)

@[simp]

theorem IsRightContinuous.const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Preorder X] [TopologicalSpace Y] {c : Y} : IsRightContinuous fun (x : X) => c

@[simp]

theorem IsLeftContinuous.const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Preorder X] [TopologicalSpace Y] {c : Y} : IsLeftContinuous fun (x : X) => c

theorem IsRightContinuous.mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Mul Y] [ContinuousMul Y] (hf : IsRightContinuous f) (hg : IsRightContinuous g) : IsRightContinuous (f * g)

theorem IsRightContinuous.add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Add Y] [ContinuousAdd Y] (hf : IsRightContinuous f) (hg : IsRightContinuous g) : IsRightContinuous (f + g)

theorem IsRightContinuous.fun_mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Mul Y] [ContinuousMul Y] (hf : IsRightContinuous f) (hg : IsRightContinuous g) : IsRightContinuous fun (i : X) => f i * g i

Eta-expanded form of IsRightContinuous.mul

theorem IsRightContinuous.fun_add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Add Y] [ContinuousAdd Y] (hf : IsRightContinuous f) (hg : IsRightContinuous g) : IsRightContinuous fun (i : X) => f i + g i

Eta-expanded form of IsRightContinuous.add

theorem IsLeftContinuous.fun_mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Mul Y] [ContinuousMul Y] (hf : IsLeftContinuous f) (hg : IsLeftContinuous g) : IsLeftContinuous fun (i : X) => f i * g i

theorem IsLeftContinuous.mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Mul Y] [ContinuousMul Y] (hf : IsLeftContinuous f) (hg : IsLeftContinuous g) : IsLeftContinuous (f * g)

theorem IsLeftContinuous.fun_add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Add Y] [ContinuousAdd Y] (hf : IsLeftContinuous f) (hg : IsLeftContinuous g) : IsLeftContinuous fun (i : X) => f i + g i

theorem IsLeftContinuous.add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Add Y] [ContinuousAdd Y] (hf : IsLeftContinuous f) (hg : IsLeftContinuous g) : IsLeftContinuous (f + g)

theorem IsRightContinuous.div' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Div Y] [ContinuousDiv Y] (hf : IsRightContinuous f) (hg : IsRightContinuous g) : IsRightContinuous (f / g)

theorem IsRightContinuous.fun_sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Sub Y] [ContinuousSub Y] (hf : IsRightContinuous f) (hg : IsRightContinuous g) : IsRightContinuous fun (i : X) => f i - g i

Eta-expanded form of IsRightContinuous.sub

theorem IsRightContinuous.fun_div' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Div Y] [ContinuousDiv Y] (hf : IsRightContinuous f) (hg : IsRightContinuous g) : IsRightContinuous fun (i : X) => f i / g i

Eta-expanded form of IsRightContinuous.div'

theorem IsLeftContinuous.fun_sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Sub Y] [ContinuousSub Y] (hf : IsLeftContinuous f) (hg : IsLeftContinuous g) : IsLeftContinuous fun (i : X) => f i - g i

theorem IsLeftContinuous.div' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Div Y] [ContinuousDiv Y] (hf : IsLeftContinuous f) (hg : IsLeftContinuous g) : IsLeftContinuous (f / g)

theorem IsLeftContinuous.sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Sub Y] [ContinuousSub Y] (hf : IsLeftContinuous f) (hg : IsLeftContinuous g) : IsLeftContinuous (f - g)

theorem IsLeftContinuous.fun_div' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Div Y] [ContinuousDiv Y] (hf : IsLeftContinuous f) (hg : IsLeftContinuous g) : IsLeftContinuous fun (i : X) => f i / g i

theorem IsRightContinuous.sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Sub Y] [ContinuousSub Y] (hf : IsRightContinuous f) (hg : IsRightContinuous g) : IsRightContinuous (f - g)

theorem IsRightContinuous.div {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [GroupWithZero Y] [ContinuousInv₀ Y] [ContinuousMul Y] (hf : IsRightContinuous f) (hg : IsRightContinuous g) (h : ∀ (x : X), g x ≠ 0) : IsRightContinuous (f / g)

theorem IsRightContinuous.fun_div {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [GroupWithZero Y] [ContinuousInv₀ Y] [ContinuousMul Y] (hf : IsRightContinuous f) (hg : IsRightContinuous g) (h : ∀ (x : X), g x ≠ 0) : IsRightContinuous fun (i : X) => f i / g i

Eta-expanded form of IsRightContinuous.div

theorem IsLeftContinuous.div {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [GroupWithZero Y] [ContinuousInv₀ Y] [ContinuousMul Y] (hf : IsLeftContinuous f) (hg : IsLeftContinuous g) (h : ∀ (x : X), g x ≠ 0) : IsLeftContinuous (f / g)

theorem IsLeftContinuous.fun_div {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [GroupWithZero Y] [ContinuousInv₀ Y] [ContinuousMul Y] (hf : IsLeftContinuous f) (hg : IsLeftContinuous g) (h : ∀ (x : X), g x ≠ 0) : IsLeftContinuous fun (i : X) => f i / g i

theorem IsRightContinuous.inv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Inv Y] [ContinuousInv Y] (hf : IsRightContinuous f) : IsRightContinuous f⁻¹

theorem IsRightContinuous.neg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Neg Y] [ContinuousNeg Y] (hf : IsRightContinuous f) : IsRightContinuous (-f)

theorem IsRightContinuous.fun_neg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Neg Y] [ContinuousNeg Y] (hf : IsRightContinuous f) : IsRightContinuous fun (i : X) => -f i

Eta-expanded form of IsRightContinuous.neg

theorem IsRightContinuous.fun_inv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Inv Y] [ContinuousInv Y] (hf : IsRightContinuous f) : IsRightContinuous fun (i : X) => (f i)⁻¹

Eta-expanded form of IsRightContinuous.inv

theorem IsLeftContinuous.fun_neg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Neg Y] [ContinuousNeg Y] (hf : IsLeftContinuous f) : IsLeftContinuous fun (i : X) => -f i

theorem IsLeftContinuous.inv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Inv Y] [ContinuousInv Y] (hf : IsLeftContinuous f) : IsLeftContinuous f⁻¹

theorem IsLeftContinuous.fun_inv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Inv Y] [ContinuousInv Y] (hf : IsLeftContinuous f) : IsLeftContinuous fun (i : X) => (f i)⁻¹

theorem IsLeftContinuous.neg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Neg Y] [ContinuousNeg Y] (hf : IsLeftContinuous f) : IsLeftContinuous (-f)

theorem IsRightContinuous.inv₀ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Zero Y] [Inv Y] [ContinuousInv₀ Y] (hf : IsRightContinuous f) (h : ∀ (x : X), f x ≠ 0) : IsRightContinuous f⁻¹

theorem IsRightContinuous.fun_inv₀ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Zero Y] [Inv Y] [ContinuousInv₀ Y] (hf : IsRightContinuous f) (h : ∀ (x : X), f x ≠ 0) : IsRightContinuous fun (i : X) => (f i)⁻¹

Eta-expanded form of IsRightContinuous.inv₀

theorem IsLeftContinuous.inv₀ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Zero Y] [Inv Y] [ContinuousInv₀ Y] (hf : IsLeftContinuous f) (h : ∀ (x : X), f x ≠ 0) : IsLeftContinuous f⁻¹

theorem IsLeftContinuous.fun_inv₀ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] [Zero Y] [Inv Y] [ContinuousInv₀ Y] (hf : IsLeftContinuous f) (h : ∀ (x : X), f x ≠ 0) : IsLeftContinuous fun (i : X) => (f i)⁻¹

theorem IsRightContinuous.const_smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [SMul R Y] [ContinuousConstSMul R Y] (c : R) (hf : IsRightContinuous f) : IsRightContinuous (c • f)

theorem IsRightContinuous.fun_const_smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [SMul R Y] [ContinuousConstSMul R Y] (c : R) (hf : IsRightContinuous f) : IsRightContinuous fun (i : X) => c • f i

Eta-expanded form of IsRightContinuous.const_smul

theorem IsLeftContinuous.fun_const_smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [SMul R Y] [ContinuousConstSMul R Y] (c : R) (hf : IsLeftContinuous f) : IsLeftContinuous fun (i : X) => c • f i

theorem IsLeftContinuous.const_smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [SMul R Y] [ContinuousConstSMul R Y] (c : R) (hf : IsLeftContinuous f) : IsLeftContinuous (c • f)

theorem IsRightContinuous.const_vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [VAdd R Y] [ContinuousConstVAdd R Y] (c : R) (hf : IsRightContinuous f) : IsRightContinuous (c +ᵥ f)

theorem IsLeftContinuous.fun_const_vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [VAdd R Y] [ContinuousConstVAdd R Y] (c : R) (hf : IsLeftContinuous f) : IsLeftContinuous fun (i : X) => c +ᵥ f i

theorem IsRightContinuous.fun_const_vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [VAdd R Y] [ContinuousConstVAdd R Y] (c : R) (hf : IsRightContinuous f) : IsRightContinuous fun (i : X) => c +ᵥ f i

theorem IsLeftContinuous.const_vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [VAdd R Y] [ContinuousConstVAdd R Y] (c : R) (hf : IsLeftContinuous f) : IsLeftContinuous (c +ᵥ f)

structure IsCaglad {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Preorder X] [TopologicalSpace Y] (f : X → Y) : Prop

A function is càglàd if it is left-continuous and has right limits.

• isLeftContinuous : IsLeftContinuous f
• tendsto_nhdsGT (x : X) : ∃ (l : Y), Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds l)

structure IsCadlag {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Preorder X] [TopologicalSpace Y] (f : X → Y) : Prop

A function is càdlàg if it is right-continuous and has left limits.

• isRightContinuous : IsRightContinuous f
• tendsto_nhdsLT (x : X) : ∃ (l : Y), Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds l)

theorem Continuous.isCadlag {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] (hf : Continuous f) : IsCadlag f

theorem Continuous.isCaglad {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] (hf : Continuous f) : IsCaglad f

@[simp]

theorem IsCadlag.const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Preorder X] [TopologicalSpace Y] {c : Y} : IsCadlag fun (x : X) => c

@[simp]

theorem IsCaglad.const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Preorder X] [TopologicalSpace Y] {c : Y} : IsCaglad fun (x : X) => c

theorem IsCadlag.continuous_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] {g : Y → Z} (hf : IsCadlag f) (hg : Continuous g) : IsCadlag (g ∘ f)

theorem IsCaglad.continuous_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] {g : Y → Z} (hf : IsCaglad f) (hg : Continuous g) : IsCaglad (g ∘ f)

theorem IsCadlag.fun_continuous_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] {g : Y → Z} (hf : IsCadlag f) (hg : Continuous g) : IsCadlag fun (x : X) => g (f x)

Eta-expanded form of IsCadlag.continuous_comp

theorem IsCaglad.fun_continuous_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] {g : Y → Z} (hf : IsCaglad f) (hg : Continuous g) : IsCaglad fun (x : X) => g (f x)

Eta-expanded form of IsCaglad.continuous_comp

theorem IsCadlag.continuous_comp₂ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} {T : Type u_4} [TopologicalSpace Z] [TopologicalSpace T] {g : X → Z} {φ : Y → Z → T} (hf : IsCadlag f) (hg : IsCadlag g) (hφ : Continuous (Function.uncurry φ)) : IsCadlag fun (x : X) => φ (f x) (g x)

theorem IsCaglad.continuous_comp₂ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {Z : Type u_3} {T : Type u_4} [TopologicalSpace Z] [TopologicalSpace T] {g : X → Z} {φ : Y → Z → T} (hf : IsCaglad f) (hg : IsCaglad g) (hφ : Continuous (Function.uncurry φ)) : IsCaglad fun (x : X) => φ (f x) (g x)

theorem IsCadlag.mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Mul Y] [ContinuousMul Y] (hf : IsCadlag f) (hg : IsCadlag g) : IsCadlag (f * g)

theorem IsCadlag.add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Add Y] [ContinuousAdd Y] (hf : IsCadlag f) (hg : IsCadlag g) : IsCadlag (f + g)

theorem IsCadlag.fun_add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Add Y] [ContinuousAdd Y] (hf : IsCadlag f) (hg : IsCadlag g) : IsCadlag fun (i : X) => f i + g i

Eta-expanded form of IsCadlag.add

theorem IsCadlag.fun_mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Mul Y] [ContinuousMul Y] (hf : IsCadlag f) (hg : IsCadlag g) : IsCadlag fun (i : X) => f i * g i

Eta-expanded form of IsCadlag.mul

theorem IsCaglad.add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Add Y] [ContinuousAdd Y] (hf : IsCaglad f) (hg : IsCaglad g) : IsCaglad (f + g)

theorem IsCaglad.fun_mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Mul Y] [ContinuousMul Y] (hf : IsCaglad f) (hg : IsCaglad g) : IsCaglad fun (i : X) => f i * g i

theorem IsCaglad.mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Mul Y] [ContinuousMul Y] (hf : IsCaglad f) (hg : IsCaglad g) : IsCaglad (f * g)

theorem IsCaglad.fun_add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Add Y] [ContinuousAdd Y] (hf : IsCaglad f) (hg : IsCaglad g) : IsCaglad fun (i : X) => f i + g i

theorem IsCadlag.div' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Div Y] [ContinuousDiv Y] (hf : IsCadlag f) (hg : IsCadlag g) : IsCadlag (f / g)

theorem IsCadlag.fun_sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Sub Y] [ContinuousSub Y] (hf : IsCadlag f) (hg : IsCadlag g) : IsCadlag fun (i : X) => f i - g i

Eta-expanded form of IsCadlag.sub

theorem IsCadlag.fun_div' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Div Y] [ContinuousDiv Y] (hf : IsCadlag f) (hg : IsCadlag g) : IsCadlag fun (i : X) => f i / g i

Eta-expanded form of IsCadlag.div'

theorem IsCaglad.fun_div' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Div Y] [ContinuousDiv Y] (hf : IsCaglad f) (hg : IsCaglad g) : IsCaglad fun (i : X) => f i / g i

theorem IsCaglad.sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Sub Y] [ContinuousSub Y] (hf : IsCaglad f) (hg : IsCaglad g) : IsCaglad (f - g)

theorem IsCaglad.fun_sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Sub Y] [ContinuousSub Y] (hf : IsCaglad f) (hg : IsCaglad g) : IsCaglad fun (i : X) => f i - g i

theorem IsCaglad.div' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Div Y] [ContinuousDiv Y] (hf : IsCaglad f) (hg : IsCaglad g) : IsCaglad (f / g)

theorem IsCadlag.sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f g : X → Y} [Preorder X] [TopologicalSpace Y] [Sub Y] [ContinuousSub Y] (hf : IsCadlag f) (hg : IsCadlag g) : IsCadlag (f - g)

theorem IsCadlag.const_smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [SMul R Y] [ContinuousConstSMul R Y] (c : R) (hf : IsCadlag f) : IsCadlag (c • f)

theorem IsCadlag.fun_const_smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [SMul R Y] [ContinuousConstSMul R Y] (c : R) (hf : IsCadlag f) : IsCadlag fun (i : X) => c • f i

Eta-expanded form of IsCadlag.const_smul

theorem IsCaglad.fun_const_smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [SMul R Y] [ContinuousConstSMul R Y] (c : R) (hf : IsCaglad f) : IsCaglad fun (i : X) => c • f i

theorem IsCaglad.const_smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [SMul R Y] [ContinuousConstSMul R Y] (c : R) (hf : IsCaglad f) : IsCaglad (c • f)

theorem IsCadlag.fun_const_vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [VAdd R Y] [ContinuousConstVAdd R Y] (c : R) (hf : IsCadlag f) : IsCadlag fun (i : X) => c +ᵥ f i

theorem IsCaglad.fun_const_vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [VAdd R Y] [ContinuousConstVAdd R Y] (c : R) (hf : IsCaglad f) : IsCaglad fun (i : X) => c +ᵥ f i

theorem IsCadlag.const_vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [VAdd R Y] [ContinuousConstVAdd R Y] (c : R) (hf : IsCadlag f) : IsCadlag (c +ᵥ f)

theorem IsCaglad.const_vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [Preorder X] [TopologicalSpace Y] {R : Type u_3} [VAdd R Y] [ContinuousConstVAdd R Y] (c : R) (hf : IsCaglad f) : IsCaglad (c +ᵥ f)

theorem IsCaglad.tendsto_nhdsGT_rightLim {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [LinearOrder X] [TopologicalSpace Y] [OrderTopology X] (hf : IsCaglad f) (x : X) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (Function.rightLim f x))

theorem IsCadlag.tendsto_nhdsLT_leftLim {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [LinearOrder X] [TopologicalSpace Y] [OrderTopology X] (hf : IsCadlag f) (x : X) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (Function.leftLim f x))

theorem IsCadlag.isLocallyBounded {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [LinearOrder X] [PseudoMetricSpace Y] (hf : IsCadlag f) (x : X) : ∃ t ∈ nhds x, Bornology.IsBounded (f '' t)

A càdlàg function is locally bounded.

theorem IsCaglad.isLocallyBounded {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [LinearOrder X] [PseudoMetricSpace Y] (hf : IsCaglad f) (x : X) : ∃ t ∈ nhds x, Bornology.IsBounded (f '' t)

A càglàd function is locally bounded.

theorem isBounded_image_of_isCadlag_of_isCompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [LinearOrder X] [PseudoMetricSpace Y] (hf : IsCadlag f) {s : Set X} (hs : IsCompact s) : Bornology.IsBounded (f '' s)

A càdlàg function maps compact sets to bounded sets.

theorem isBounded_image_of_isCaglad_of_isCompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} [LinearOrder X] [PseudoMetricSpace Y] (hf : IsCaglad f) {s : Set X} (hs : IsCompact s) : Bornology.IsBounded (f '' s)

A càglàd function maps compact sets to bounded sets.