cadlag functions #
@[reducible, inline]
abbrev
Function.RightContinuous
{ι : Type u_1}
{E : Type u_2}
[PartialOrder ι]
[TopologicalSpace ι]
[TopologicalSpace E]
(f : ι → E)
:
The predicate that a function is right continuous.
Equations
- Function.RightContinuous f = ∀ (a : ι), ContinuousWithinAt f (Set.Ioi a) a
Instances For
structure
IsCadlag
{ι : Type u_1}
{E : Type u_2}
[PartialOrder ι]
[TopologicalSpace ι]
[TopologicalSpace E]
(f : ι → E)
:
A function is cadlag if it is right-continuous and has left limits.
- right_continuous : Function.RightContinuous f
- left_limit (x : ι) : ∃ (l : E), Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds l)
Instances For
theorem
isBounded_image_of_isCadlag_of_isCompact
{ι : Type u_1}
[PartialOrder ι]
[TopologicalSpace ι]
{E : Type u_3}
[FirstCountableTopology ι]
[PseudoMetricSpace E]
{f : ι → E}
(hf : IsCadlag f)
{s : Set ι}
(hs : IsCompact s)
:
Bornology.IsBounded (f '' s)
A càdlàg function maps compact sets to bounded sets.