Add measurable_Rbar_gen_lub_up_{m,p}.

Lebesgue/measurable_Rbar.v

@@ -287,6 +287,50 @@ repeat apply measurable_union; easy.
 rewrite up_id_union_seq; apply measurable_union_seq; easy.
 Qed.
 
+Inductive Up_m_G : (Rbar -> Prop) -> Prop :=
+  UG_m : forall A, G A -> Up_m_G (up_m A).
+
+Hypothesis measurable_Up_m_G_singleton :
+  forall y, measurable Up_m_G (singleton y).
+
+Lemma measurable_Rbar_gen_lub_up_m :
+  Incl (measurable G) (fun A => measurable Up_m_G (up_m A)).
+Proof.
+intros A HA; induction HA as [A HA | | A HA | A HA1 HA2].
+apply measurable_gen; easy.
+apply measurable_union; try easy.
+rewrite up_id_empty; apply measurable_empty.
+rewrite up_m_compl; apply measurable_compl.
+apply measurable_union; try easy.
+apply measurable_ext with (diff (up_m A) (singleton m_infty)).
+Rbar_subset_full_unfold; intros y; destruct y; simpl; repeat split;
+    intros; try easy; tauto.
+apply measurable_diff; easy.
+rewrite up_m_union_seq; apply measurable_union_seq; easy.
+Qed.
+
+Inductive Up_p_G : (Rbar -> Prop) -> Prop :=
+  UG_p : forall A, G A -> Up_p_G (up_p A).
+
+Hypothesis measurable_Up_p_G_singleton :
+  forall y, measurable Up_p_G (singleton y).
+
+Lemma measurable_Rbar_gen_lub_up_p :
+  Incl (measurable G) (fun A => measurable Up_p_G (up_p A)).
+Proof.
+intros A HA; induction HA as [A HA | | A HA | A HA1 HA2].
+apply measurable_gen; easy.
+apply measurable_union; try easy.
+rewrite up_id_empty; apply measurable_empty.
+rewrite up_p_compl; apply measurable_compl.
+apply measurable_union; try easy.
+apply measurable_ext with (diff (up_p A) (singleton p_infty)).
+Rbar_subset_full_unfold; intros y; destruct y; simpl; repeat split;
+    intros; try easy; tauto.
+apply measurable_diff; easy.
+rewrite up_p_union_seq; apply measurable_union_seq; easy.
+Qed.
+
 Inductive Up_mp_G : (Rbar -> Prop) -> Prop :=
   UG_mp : forall A, G A -> Up_mp_G (up_mp A).