fact: Definition expand_U_dyadic (f:nat->Ensemble X) (Hopen: forall n:nat, open (f n)) (Hincr: forall n:nat, Included (closure (f n)) (f (S n))) (n:nat) : Ensemble X := if (even_odd_dec n) then f (div2 n) else let m := div2 n in proj1_sig (normal_sep_fun (closure (f m)) (f (S m)) (closure_closed _) (Hopen _) (Hincr _)).
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology