include "lebesgue.ma".
include "models/nat_order_continuous.ma".
-alias symbol "pair" = "dependent pair".
theorem nat_lebesgue_oc:
- ∀a:sequence ℕ.∀l,u:nat_ordered_uniform_space.∀H:∀i:nat.a i ∈ [l,u].
+ ∀a:sequence ℕ.∀l,u:ℕ.∀H:∀i:nat.a i ∈ [l,u].
∀x:ℕ.a order_converges x →
x ∈ [l,u] ∧
∀h:x ∈ [l,u].
- uniform_converge {[l,u]} (⌊n,〈a n,H n〉⌋) 〈x,h〉.
+ uniform_converge {[l,u]} ⌊n,≪a n,H n≫⌋ ≪x,h≫.
intros; apply lebesgue_oc; [apply nat_us_is_oc] assumption;
qed.