fact: Definition U_dyadic_level_n (n:nat) : { f:nat->Ensemble X | (forall m:nat, open (f m)) /\ (forall m:nat, Included (closure (f m)) (f (S m))) }.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology