Skip to content
Snippets Groups Projects
Commit ad49acf0 authored by François Clément's avatar François Clément
Browse files

Implement Subset_seq.v from new Subset_any.v.

parent 5eabc58a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Lebesgue/Subset_seq.v
+ 62
− 144
View file @ ad49acf0
......@@ -27,7 +27,7 @@ From Coq Require Import Classical FunctionalExtensionality FinFun.
From Coq Require Import Arith Lia Even.
Require Import countable_sets nat_compl.
Require Import Subset Subset_finite.
Require Import Subset Subset_finite Subset_any.
Section Def0.
......@@ -52,11 +52,8 @@ Variable phi : nat -> nat * nat.
(** Binary and unary predicates on sequences of subsets. *)
Definition incl_seq : Prop :=
forall n, incl (A n) (B n).
Definition same_seq : Prop :=
forall n, same (A n) (B n). (* Should it be A n = B n? *)
Definition incl_seq : Prop := @incl_any U nat A B.
Definition same_seq : Prop := @same_any U nat A B.
(* Warning: incr actually means nondecreasing. *)
Definition incr_seq : Prop :=
......@@ -74,19 +71,15 @@ Definition disj_seq_alt : Prop :=
(** Unary and binary operations on sequences of subsets. *)
Definition compl_seq : nat -> U -> Prop :=
fun n => compl (A n).
Definition compl_seq : nat -> U -> Prop := @compl_any U nat A.
Definition x_inter_seq : nat -> U -> Prop :=
fun n => inter (A (fst (phi n))) (B (snd (phi n))).
(** Reduce operations on sequences of subsets. *)
Definition union_seq : U -> Prop :=
fun x => exists n, A n x.
Definition inter_seq : U -> Prop :=
fun x => forall n, A n x.
Definition union_seq : U -> Prop := @union_any U nat A.
Definition inter_seq : U -> Prop := @inter_any U nat A.
(** Predicate on sequences of subsets. *)
......@@ -105,11 +98,8 @@ Variable B2 : U2 -> Prop. (* Subset. *)
Variable B1 : U1 -> Prop. (* Subset. *)
Variable A2 : nat -> U2 -> Prop. (* Subset sequence. *)
Definition prod_seq_l : nat -> U1 * U2 -> Prop :=
fun n => prod (A1 n) B2.
Definition prod_seq_r : nat -> U1 * U2 -> Prop :=
fun n => prod B1 (A2 n).
Definition prod_seq_l : nat -> U1 * U2 -> Prop := @prod_any_l U1 U2 nat A1 B2.
Definition prod_seq_r : nat -> U1 * U2 -> Prop := @prod_any_r U1 U2 nat B1 A2.
End Seq_Def2.
......@@ -124,18 +114,14 @@ Lemma subset_seq_ext :
forall (A B : nat -> U -> Prop),
same_seq A B -> A = B.
Proof.
intros A B H.
apply functional_extensionality; intros n.
apply subset_ext, H.
apply subset_any_ext.
Qed.
Lemma subset_seq_ext_equiv :
forall (A B : nat -> U -> Prop),
A = B <-> incl_seq A B /\ incl_seq B A.
Proof.
intros; split.
intros H; split; now rewrite H.
intros [H1 H2]; apply subset_seq_ext; split; [apply H1 | apply H2].
apply subset_any_ext_equiv.
Qed.
End Seq_Facts0.
......@@ -149,7 +135,7 @@ Ltac subset_seq_unfold :=
x_inter_seq, compl_seq. (* Operators. *)
Ltac subset_seq_full_unfold :=
subset_seq_unfold; subset_finite_full_unfold.
subset_seq_unfold; subset_any_unfold; subset_finite_full_unfold.
Ltac subset_seq_auto :=
subset_seq_unfold; try easy; try tauto; auto.
......@@ -225,25 +211,21 @@ Lemma incl_seq_refl :
forall (A B : nat -> U -> Prop),
same_seq A B -> incl_seq A B.
Proof.
intros A B; rewrite same_seq_equiv_def, incl_seq_equiv_def.
intros H N; now apply incl_finite_refl.
apply incl_any_refl.
Qed.
Lemma incl_seq_antisym :
forall (A B : nat -> U -> Prop),
incl_seq A B -> incl_seq B A -> same_seq A B.
Proof.
intros A B H1 H2.
assert (HH : A = B -> same_seq A B).
intros H'; now rewrite H'.
now apply HH, subset_seq_ext_equiv.
apply incl_any_antisym.
Qed.
Lemma incl_seq_trans :
forall (A B C : nat -> U -> Prop),
incl_seq A B -> incl_seq B C -> incl_seq A C.
Proof.
intros A B C H1 H2 n x Hx; now apply H2, H1.
apply incl_any_trans.
Qed.
(** same_seq is an equivalence binary relation. *)
......@@ -260,16 +242,14 @@ Lemma same_seq_sym :
forall (A B : nat -> U -> Prop),
same_seq A B -> same_seq B A.
Proof.
intros A B H n; apply same_sym, (H n).
apply same_any_sym.
Qed.
Lemma same_seq_trans :
forall (A B C : nat -> U -> Prop),
same_seq A B -> same_seq B C -> same_seq A C.
Proof.
intros A B C H1 H2 n; apply same_trans with (B n).
apply (H1 n).
apply (H2 n).
apply same_any_trans.
Qed.
(** Facts about incr_seq and decr_seq. *)
......@@ -529,8 +509,7 @@ Lemma compl_seq_invol :
forall (A : nat -> U -> Prop),
compl_seq (compl_seq A) = A.
Proof.
intros; apply subset_seq_ext.
intros n x; subset_seq_full_auto.
subset_seq_unfold; apply compl_any_invol.
Qed.
Lemma compl_seq_shift :
......@@ -544,34 +523,28 @@ Lemma compl_seq_monot :
forall (A B : nat -> U -> Prop),
incl_seq A B -> incl_seq (compl_seq B) (compl_seq A).
Proof.
subset_seq_unfold; intros; now apply compl_monot, H.
subset_seq_unfold; apply compl_any_monot.
Qed.
Lemma incl_compl_seq_equiv :
forall (A B : nat -> U -> Prop),
incl_seq A B <-> incl_seq (compl_seq B) (compl_seq A).
Proof.
intros; split.
apply compl_seq_monot.
rewrite <- (compl_seq_invol A) at 2; rewrite <- (compl_seq_invol B) at 2.
apply compl_seq_monot.
subset_seq_unfold; apply incl_compl_any_equiv.
Qed.
Lemma same_compl_seq :
forall (A B : nat -> U -> Prop),
same_seq A B -> same_seq (compl_seq A) (compl_seq B).
Proof.
intros A B H n; apply same_compl, H.
subset_seq_unfold; apply same_compl_any.
Qed.
Lemma same_compl_seq_equiv :
forall (A B : nat -> U -> Prop),
same_seq A B <-> same_seq (compl_seq A) (compl_seq B).
Proof.
intros; split.
apply same_compl_seq.
rewrite <- (compl_seq_invol A) at 2; rewrite <- (compl_seq_invol B) at 2.
apply same_compl_seq.
subset_seq_unfold; apply same_compl_any_equiv.
Qed.
Lemma incr_compl_seq :
......@@ -594,7 +567,7 @@ Lemma compl_seq_reg :
forall (A B : nat -> U -> Prop),
same_seq (compl_seq A) (compl_seq B) -> A = B.
Proof.
intros; now apply subset_seq_ext, same_compl_seq_equiv.
subset_seq_unfold; apply compl_any_reg.
Qed.
(** Facts about x_inter_seq. *)
......@@ -648,9 +621,7 @@ Lemma union_seq_empty :
forall (A : nat -> U -> Prop),
union_seq A = emptyset <-> forall n, A n = emptyset.
Proof.
intros A; rewrite <- empty_emptyset; split; intros H.
intros n; rewrite <- empty_emptyset; intros x Hx; apply (H x); now exists n.
intros x [n Hx]; specialize (H n); rewrite <- empty_emptyset in H; now apply (H x).
apply union_any_empty.
Qed.
Lemma union_seq_monot :
......@@ -658,14 +629,14 @@ Lemma union_seq_monot :
incl_seq A B ->
incl (union_seq A) (union_seq B).
Proof.
intros A B H x [n Hx]; exists n; now apply H.
apply union_any_monot.
Qed.
Lemma union_seq_ub :
forall (A : nat -> U -> Prop) n,
incl (A n) (union_seq A).
Proof.
intros A n x Hx; now exists n.
apply union_any_ub.
Qed.
Lemma union_seq_full :
......@@ -673,9 +644,7 @@ Lemma union_seq_full :
(exists n, A n = fullset) ->
union_seq A = fullset.
Proof.
intros A [n HAn].
apply subset_ext_equiv; split; try easy.
rewrite <- HAn; now apply union_seq_ub.
apply union_any_full.
Qed.
Lemma union_seq_lub :
......@@ -683,7 +652,7 @@ Lemma union_seq_lub :
(forall n, incl (A n) B) ->
incl (union_seq A) B.
Proof.
intros A B H x [n Hx]; now apply (H n).
apply union_any_lub.
Qed.
Lemma incl_union_seq :
......@@ -691,7 +660,7 @@ Lemma incl_union_seq :
incl (union_seq A) B ->
forall n, incl (A n) B.
Proof.
intros A B H n x Hx; apply H; now exists n.
apply incl_union_any.
Qed.
Lemma union_seq_incl_compat :
......@@ -717,38 +686,28 @@ Lemma union_union_seq_distr_l :
forall (A : U -> Prop) (B : nat -> U -> Prop),
union A (union_seq B) = union_seq (fun n => union A (B n)).
Proof.
intros A B; apply subset_ext; intros x; split.
intros [Hx | [n Hx]]; [exists 0; now left | exists n; now right].
intros [n [Hx | Hx]]; [now left | right; now exists n].
apply union_union_any_distr_l, inhabited_nat.
Qed.
Lemma union_union_seq_distr_r :
forall (A : nat -> U -> Prop) (B : U -> Prop),
union (union_seq A) B = union_seq (fun n => union (A n) B).
Proof.
intros; rewrite union_comm, union_union_seq_distr_l.
apply union_seq_eq_compat; intros.
rewrite <- union_union_finite_distr_l, union_comm.
apply union_union_finite_distr_r.
apply union_union_any_distr_r, inhabited_nat.
Qed.
Lemma inter_union_seq_distr_l :
forall (A : U -> Prop) (B : nat -> U -> Prop),
inter A (union_seq B) = union_seq (fun n => inter A (B n)).
Proof.
intros A B; apply subset_ext; intros x; split.
intros [Hx1 [n Hx2]]; now exists n.
intros [n [Hx1 Hx2]]; split; [easy | now exists n].
apply inter_union_any_distr_l.
Qed.
Lemma inter_union_seq_distr_r :
forall (A : nat -> U -> Prop) (B : U -> Prop),
inter (union_seq A) B = union_seq (fun n => inter (A n) B).
Proof.
intros; rewrite inter_comm, inter_union_seq_distr_l.
apply union_seq_eq_compat; intros.
rewrite <- inter_union_finite_distr_l, inter_comm.
apply inter_union_finite_distr_r.
apply inter_union_any_distr_r.
Qed.
Lemma inter_union_seq_distr :
......@@ -834,9 +793,7 @@ Lemma inter_seq_full :
forall (A : nat -> U -> Prop),
inter_seq A = fullset <-> forall n, A n = fullset.
Proof.
intros A; rewrite <- full_fullset; split; intros H.
intros n; rewrite <- full_fullset; intros x; now apply (H x).
intros x n; specialize (H n); rewrite <- full_fullset in H; now apply (H x).
apply inter_any_full.
Qed.
Lemma inter_seq_monot :
......@@ -844,7 +801,7 @@ Lemma inter_seq_monot :
incl_seq A B ->
incl (inter_seq A) (inter_seq B).
Proof.
intros A B H x Hx n; apply H, Hx.
apply inter_any_monot.
Qed.
Lemma inter_seq_empty :
......@@ -852,9 +809,7 @@ Lemma inter_seq_empty :
(exists n, A n = emptyset) ->
inter_seq A = emptyset.
Proof.
intros A [n HAn].
apply subset_ext_equiv; split; try easy.
now rewrite <- HAn.
apply inter_any_empty.
Qed.
Lemma inter_seq_glb :
......@@ -862,7 +817,7 @@ Lemma inter_seq_glb :
(forall n, incl B (A n)) ->
incl B (inter_seq A).
Proof.
intros A B H x Hx n; now apply H.
apply inter_any_glb.
Qed.
Lemma incl_inter_seq :
......@@ -870,7 +825,7 @@ Lemma incl_inter_seq :
incl B (inter_seq A) ->
forall n, incl B (A n).
Proof.
intros A B H n x Hx; now apply H.
apply incl_inter_any.
Qed.
Lemma inter_seq_incl_compat :
......@@ -896,40 +851,28 @@ Lemma union_inter_seq_distr_l :
forall (A : U -> Prop) (B : nat -> U -> Prop),
union A (inter_seq B) = inter_seq (fun n => union A (B n)).
Proof.
intros A B; apply subset_ext; intros x; split.
intros [Hx | Hx] n; [now left | right; apply Hx].
intros Hx1; case (classic (A x)); intros Hx2.
now left.
right; intros n; now destruct (Hx1 n).
apply union_inter_any_distr_l.
Qed.
Lemma union_inter_seq_distr_r :
forall (A : nat -> U -> Prop) (B : U -> Prop),
union (inter_seq A) B = inter_seq (fun n => union (A n) B).
Proof.
intros; rewrite union_comm, union_inter_seq_distr_l.
apply inter_seq_eq_compat; intros.
rewrite <- union_inter_finite_distr_l, union_comm.
apply union_inter_finite_distr_r.
apply union_inter_any_distr_r.
Qed.
Lemma inter_inter_seq_distr_l :
forall (A : U -> Prop) (B : nat -> U -> Prop),
inter A (inter_seq B) = inter_seq (fun n => inter A (B n)).
Proof.
intros A B; apply subset_ext; intros x; split.
intros [Hx1 Hx2] n; split; [easy | apply Hx2].
intros Hx; split; [apply (Hx 0) | intros n; apply (Hx n)].
apply inter_inter_any_distr_l, inhabited_nat.
Qed.
Lemma inter_inter_seq_distr_r :
forall (A : nat -> U -> Prop) (B : U -> Prop),
inter (inter_seq A) B = inter_seq (fun n => inter (A n) B).
Proof.
intros; rewrite inter_comm, inter_inter_seq_distr_l.
apply inter_seq_eq_compat; intros.
rewrite <- inter_inter_finite_distr_l, inter_comm.
apply inter_inter_finite_distr_r.
apply inter_inter_any_distr_r, inhabited_nat.
Qed.
(*
......@@ -974,7 +917,7 @@ Lemma incl_inter_union_seq :
forall (A : nat -> U -> Prop),
incl (inter_seq A) (union_seq A).
Proof.
intros A x Hx; exists 0; apply (Hx 0).
apply incl_inter_union_any, inhabited_nat.
Qed.
(** De Morgan's laws. *)
......@@ -983,17 +926,14 @@ Lemma compl_union_seq :
forall (A : nat -> U -> Prop),
compl (union_seq A) = inter_seq (compl_seq A).
Proof.
intros; apply subset_ext; split.
intros H n Hx; apply H; now exists n.
intros H [n Hx]; now apply (H n).
subset_seq_unfold; apply compl_union_any.
Qed.
Lemma compl_inter_seq :
forall (A : nat -> U -> Prop),
compl (inter_seq A) = union_seq (compl_seq A).
Proof.
intros; apply compl_reg; rewrite compl_union_seq.
now rewrite compl_invol, compl_seq_invol.
subset_seq_unfold; apply compl_inter_any.
Qed.
Lemma compl_seq_union_seq :
......@@ -1004,8 +944,7 @@ Lemma compl_seq_union_seq :
compl_seq (fun n => union_seq (f A n)) =
(fun n => inter_seq (f (compl_seq A) n)).
Proof.
intros A f Hf; apply subset_seq_ext; intros n x; unfold compl_seq.
now rewrite compl_union_seq, Hf.
subset_seq_unfold; apply compl_any_union_any.
Qed.
Lemma compl_seq_inter_seq :
......@@ -1016,8 +955,7 @@ Lemma compl_seq_inter_seq :
compl_seq (fun n => inter_seq (f A n)) =
(fun n => union_seq (f (compl_seq A) n)).
Proof.
intros A f Hf; apply subset_seq_ext; intros n x; unfold compl_seq.
now rewrite compl_inter_seq, Hf.
subset_seq_unfold; apply compl_any_inter_any.
Qed.
(** ``Distributivity'' of diff. *)
......@@ -1026,14 +964,14 @@ Lemma diff_union_seq_distr_l :
forall (A : nat -> U -> Prop) (B : U -> Prop),
diff (union_seq A) B = union_seq (fun n => diff (A n) B).
Proof.
intros; now rewrite diff_equiv_def_inter, inter_union_seq_distr_r.
apply diff_union_any_distr_l.
Qed.
Lemma diff_union_seq_r :
forall (A : U -> Prop) (B : nat -> U -> Prop),
diff A (union_seq B) = inter_seq (fun n => diff A (B n)).
Proof.
intros; now rewrite diff_equiv_def_inter, compl_union_seq, inter_inter_seq_distr_l.
apply diff_union_any_r, inhabited_nat.
Qed.
Lemma diff_union_seq :
......@@ -1041,8 +979,7 @@ Lemma diff_union_seq :
diff (union_seq A) (union_seq B) =
union_seq (fun n => inter_seq (fun m => diff (A n) (B m))).
Proof.
intros; rewrite diff_union_seq_distr_l; f_equal.
apply functional_extensionality; intros; apply diff_union_seq_r.
apply diff_union_any, inhabited_nat.
Qed.
Lemma diff_union_seq_alt :
......@@ -1050,22 +987,21 @@ Lemma diff_union_seq_alt :
diff (union_seq A) (union_seq B) =
inter_seq (fun m => union_seq (fun n => diff (A n) (B m))).
Proof.
intros; rewrite diff_union_seq_r; f_equal.
apply functional_extensionality; intros; apply diff_union_seq_distr_l.
apply diff_union_any_alt, inhabited_nat.
Qed.
Lemma diff_inter_seq_distr_l :
forall (A : nat -> U -> Prop) (B : U -> Prop),
diff (inter_seq A) B = inter_seq (fun n => diff (A n) B).
Proof.
intros; now rewrite diff_equiv_def_inter, inter_inter_seq_distr_r.
apply diff_inter_any_distr_l, inhabited_nat.
Qed.
Lemma diff_inter_seq_r :
forall (A : U -> Prop) (B : nat -> U -> Prop),
diff A (inter_seq B) = union_seq (fun n => diff A (B n)).
Proof.
intros; now rewrite diff_equiv_def_inter, compl_inter_seq, inter_union_seq_distr_l.
apply diff_inter_any_r.
Qed.
Lemma diff_inter_seq :
......@@ -1073,8 +1009,7 @@ Lemma diff_inter_seq :
diff (inter_seq A) (inter_seq B) =
inter_seq (fun n => union_seq (fun m => diff (A n) (B m))).
Proof.
intros; rewrite diff_inter_seq_distr_l; f_equal.
apply functional_extensionality; intros; apply diff_inter_seq_r.
apply diff_inter_any, inhabited_nat.
Qed.
Lemma diff_inter_seq_alt :
......@@ -1082,8 +1017,7 @@ Lemma diff_inter_seq_alt :
diff (inter_seq A) (inter_seq B) =
union_seq (fun m => inter_seq (fun n => diff (A n) (B m))).
Proof.
intros; rewrite diff_inter_seq_r; f_equal.
apply functional_extensionality; intros; apply diff_inter_seq_distr_l.
apply diff_inter_any_alt, inhabited_nat.
Qed.
Lemma diff_union_inter_seq :
......@@ -1091,8 +1025,7 @@ Lemma diff_union_inter_seq :
diff (union_seq A) (inter_seq B) =
union_seq (fun n => union_seq (fun m => diff (A n) (B m))).
Proof.
intros; rewrite diff_union_seq_distr_l; f_equal.
apply functional_extensionality; intros; apply diff_inter_seq_r.
apply diff_union_inter_any.
Qed.
Lemma diff_union_inter_seq_alt :
......@@ -1100,8 +1033,7 @@ Lemma diff_union_inter_seq_alt :
diff (union_seq A) (inter_seq B) =
union_seq (fun m => union_seq (fun n => diff (A n) (B m))).
Proof.
intros; rewrite diff_inter_seq_r; f_equal.
apply functional_extensionality; intros; apply diff_union_seq_distr_l.
apply diff_union_inter_any_alt.
Qed.
Lemma diff_inter_union_seq :
......@@ -1109,8 +1041,7 @@ Lemma diff_inter_union_seq :
diff (inter_seq A) (union_seq B) =
inter_seq (fun n => inter_seq (fun m => diff (A n) (B m))).
Proof.
intros; rewrite diff_inter_seq_distr_l; f_equal.
apply functional_extensionality; intros; apply diff_union_seq_r.
apply diff_inter_union_any, inhabited_nat.
Qed.
Lemma diff_inter_union_seq_alt :
......@@ -1118,8 +1049,7 @@ Lemma diff_inter_union_seq_alt :
diff (inter_seq A) (union_seq B) =
inter_seq (fun m => inter_seq (fun n => diff (A n) (B m))).
Proof.
intros; rewrite diff_union_seq_r; f_equal.
apply functional_extensionality; intros; apply diff_inter_seq_distr_l.
apply diff_inter_union_any_alt, inhabited_nat.
Qed.
(** Facts about partition_seq. *)
......@@ -1168,10 +1098,7 @@ Lemma prod_union_seq_full :
prod (union_seq A1) (@fullset U2) =
union_seq (prod_seq_l A1 fullset).
Proof.
intros; apply subset_ext; subset_seq_full_unfold.
intros A; split.
intros [[n HA] _]; now exists n.
intros [n [HA _]]; split; now try exists n.
apply prod_union_any_full.
Qed.
Lemma prod_full_union_seq :
......@@ -1179,10 +1106,7 @@ Lemma prod_full_union_seq :
prod (@fullset U1) (union_seq A2) =
union_seq (prod_seq_r fullset A2).
Proof.
intros; apply subset_ext; subset_seq_full_unfold.
intros A; split.
intros [_ [n HA]]; now exists n.
intros [n [_ HA]]; split; now try exists n.
apply prod_full_union_any.
Qed.
Lemma prod_inter_seq_full :
......@@ -1190,10 +1114,7 @@ Lemma prod_inter_seq_full :
prod (inter_seq A1) (@fullset U2) =
inter_seq (prod_seq_l A1 fullset).
Proof.
intros; apply subset_ext; subset_seq_full_unfold.
intros A; split.
intros [HA _] n; split; now try apply (HA n).
intros HA; split; try easy; apply HA.
apply prod_inter_any_full.
Qed.
Lemma prod_full_inter_seq :
......@@ -1201,10 +1122,7 @@ Lemma prod_full_inter_seq :
prod (@fullset U1) (inter_seq A2) =
inter_seq (prod_seq_r fullset A2).
Proof.
intros; apply subset_ext; subset_seq_full_unfold.
intros A; split.
intros [_ HA] n; split; now try apply (HA n).
intros HA; split; try easy; apply HA.
apply prod_full_inter_any.
Qed.
End Prod_Facts.
......
Lebesgue/Tonelli.v
+ 6
− 5
View file @ ad49acf0
......@@ -28,7 +28,8 @@ From Coq Require Import PropExtensionality FunctionalExtensionality Classical.
From Coquelicot Require Import Coquelicot.
Require Import Rbar_compl sum_Rbar_nonneg.
Require Import Subset Subset_charac Subset_seq Subset_system_base Subset_system.
Require Import Subset Subset_charac Subset_any Subset_seq.
Require Import Subset_system_base Subset_system.
Require Import sigma_algebra sigma_algebra_R_Rbar.
Require Import measurable_fun measure simple_fun Mp LInt_p.
......@@ -658,7 +659,7 @@ Lemma meas_prod_uniqueness_aux2 :
(forall n, mu (A n) = nu (A n)) ->
mu (inter_seq A) = nu (inter_seq A).
Proof.
intros A HA1 HA2 HA3; unfold inter_seq; unfold decr_seq in HA2.
intros A HA1 HA2 HA3; unfold inter_seq, inter_any; unfold decr_seq in HA2.
rewrite 2!measure_continuous_from_above; try easy.
apply Inf_seq_ext; intros; apply HA3.
1,2: exists 0%nat; apply finite_measure_is_finite; try easy;
......@@ -671,7 +672,7 @@ Lemma meas_prod_uniqueness_aux3 :
(forall n, mu (A n) = nu (A n)) ->
mu (union_seq A) = nu (union_seq A).
Proof.
intros A HA1 HA2 HA3; unfold union_seq; unfold incr_seq in HA2.
intros A HA1 HA2 HA3; unfold union_seq, union_any; unfold incr_seq in HA2.
rewrite 2!measure_continuous_from_below; try easy.
apply Sup_seq_ext; intros; apply HA3.
Qed.
......@@ -721,7 +722,7 @@ pose (mun := fun n => meas_restricted _ mu (B n) (HB1 n)).
pose (nun := fun n => meas_restricted _ nu (B n) (HB1 n)).
replace A with (inter A (union_seq B)).
rewrite inter_union_seq_distr_l.
unfold union_seq; rewrite 2!measure_continuous_from_below.
unfold union_seq, union_any; rewrite 2!measure_continuous_from_below.
apply Sup_seq_ext; intros n.
apply trans_eq with (mun n A).
unfold mun, meas_restricted, meas_restricted_meas; simpl.
......@@ -765,7 +766,7 @@ intros n X; apply inter_incr_seq_compat_l; try easy.
replace (union_seq B) with (@fullset (X1*X2)).
apply inter_full_r.
apply sym_eq, functional_extensionality.
unfold union_seq, fullset.
unfold union_seq, union_any, fullset.
intros x.
apply propositional_extensionality; easy.
Qed.
......
Lebesgue/nat_compl.v
+ 10
− 0
View file @ ad49acf0
......@@ -20,6 +20,16 @@ From Coq Require Import Arith Nat Lia.
From Coquelicot Require Import Coquelicot.
Section nat_compl.
Lemma inhabited_nat : inhabited nat.
Proof.
apply (inhabits 0).
Qed.
End nat_compl.
Section Order_compl.
(** Complements on the order on natural numbers. **)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment