TendstoUniformlyOn on ordered spaces #
We gather some results about TendstoUniformlyOn f g K on ordered spaces,
in particular bounding the values of f in terms of bounds on the limit g.
theorem
TendstoUniformlyOn.eventually_forall_lt
{α : Type u_1}
{ι : Type u_2}
{β : Type u_3}
[UniformSpace β]
[AddGroup β]
[IsUniformAddGroup β]
[PartialOrder β]
[OrderTopology β]
[AddLeftMono β]
[AddRightMono β]
{f : ι → α → β}
{g : α → β}
{K : Set α}
{p : Filter ι}
{u v : β}
(huv : u < v)
(hf : TendstoUniformlyOn f g p K)
(hg : ∀ x ∈ K, g x ≤ u)
:
If a sequence of functions converges uniformly on a set to a function g which is bounded above
by a value u, then the sequence is strictly bounded by any v such that u < v.
theorem
TendstoUniformlyOn.eventually_forall_le
{α : Type u_1}
{ι : Type u_2}
{β : Type u_3}
[UniformSpace β]
[AddGroup β]
[IsUniformAddGroup β]
[PartialOrder β]
[OrderTopology β]
[AddLeftMono β]
[AddRightMono β]
{f : ι → α → β}
{g : α → β}
{K : Set α}
{p : Filter ι}
{u v : β}
(huv : u < v)
(hf : TendstoUniformlyOn f g p K)
(hg : ∀ x ∈ K, g x ≤ u)
: