Theorems · Theorem · general topology

TendstoUniformlyOn.eventually_forall_lt

∀ {α : Type u_1} {ι : Type u_2} {β : Type u_3} [inst : UniformSpace β] [inst_1 : AddGroup β] [IsUniformAddGroup β]
  [inst_3 : PartialOrder β] [OrderTopology β] [AddLeftMono β] [AddRightMono β] {f : ι → α → β} {g : α → β} {K : Set α}
  {p : Filter ι} {u v : β},
  u < v → TendstoUniformlyOn f g p K → (∀ 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.

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Order

Cited by

1 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpaceAddGroupIsUniformAddGroupPartialOrderOrderTopologyAddLeftMonoAddRightMono