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) : ∀ᶠ (i : ι) in p, ∀ x ∈ K, f i x < v

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) : ∀ᶠ (i : ι) in p, ∀ x ∈ K, f i x ≤ v