proposition: Lemma family_P1 : forall (f:family) (D:R -> Prop), family_open_set f -> family_open_set (subfamily f D).
proof: Proof. unfold family_open_set; intros; unfold subfamily; simpl; assert (H0 := classic (D x)). elim H0; intro. - cut (open_set (f0 x) -> open_set (fun y:R => f0 x y /\ D x)). + intro; apply H2; apply H. + unfold open_set; unfold neighbourhood; intros; elim H3; intros; assert (H6 := H2 _ H4); elim H6; intros; exists x1; unfold included; intros; split. * apply (H7 _ H8). * assumption. - cut (open_set (fun y:R => False) -> open_set (fun y:R => f0 x y /\ D x)). + intro; apply H2; apply open_set_P4. + unfold open_set; unfold neighbourhood; intros; elim H3; intros; elim H1; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type