fact: Definition mixed_continuous I A B (M:family I B) (S:I->A->B->Prop) := forall i x y1 y2, S i x y1 -> (forall j, family_r M j i -> family_sim M j y1 y2) -> S i x y2.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)