proposition: Lemma filterlim_switch_dom {T1 T2 : Type} {U : CompleteSpace} F1 (FF1 : ProperFilter F1) F2 (FF2 : Filter F2) (dom : T2 -> Prop) (HF2 : forall P, F2 P -> exists x, dom x /\ P x) (f : T1 -> T2 -> U) g h : filterlim (fun x (y : {z : T2 | dom z}) => f x (proj1_sig y)) F1 (locally (T := fct_UniformSpace _ _) (fun y : {z : T2 | dom z} => g (proj1_sig y))) -> (forall x, filterlim (f x) (within dom F2) (locally (h x))) -> exists l : U, filterlim h F1 (locally l) /\ filterlim g (within dom F2) (locally l).
proof: Proof. set (T2' := { y : T2 | dom y }). set (f' := fun x (y : T2') => f x (proj1_sig y)). set (F2' := fun P : T2' -> Prop => F2 (fun x => forall (H:dom x), P (exist _ x H))). set (g' := fun y : T2' => g (proj1_sig y)). intros Hfg Hfh. refine (filterlim_switch F1 FF1 F2' _ f' g' h _ _). now apply subset_filter_proper. intros H P. now apply Hfg. intros x P HP. now apply Hfh. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub