include "lebesgue.ma".
include "models/nat_order_continuous.ma".
-alias symbol "pair" = "dependent pair".
theorem nat_lebesgue_oc:
∀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]} â\8c\8an,â\8c©a n,H nâ\8cªâ\8c\8b â\8c©x,hâ\8cª.
+ uniform_converge {[l,u]} â\8c\8an,â\89ªa n,H nâ\89«â\8c\8b â\89ªx,hâ\89«.
intros; apply lebesgue_oc; [apply nat_us_is_oc] assumption;
qed.