Library Lebesgue.Subset_system

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Support for subset systems.

Used logic axioms



From Subsets Require Import Subsets_wDep Subset_finite Subset_seq.
From Lebesgue Require Import Subset_system_def Subset_system_base Subset_system_gen.

Section Subset_systems_Def1.

Context {U : Type}.
Variable gen : (U Prop) Prop. Variable A0 : U Prop.
Inductive Psyst : (U Prop) Prop :=
  | Psyst_Gen : Incl gen Psyst
  | Psyst_Mem : Psyst A0
  | Psyst_Inter : Inter Psyst.

Inductive Ring : (U Prop) Prop :=
  | Ring_Gen : Incl gen Ring
  | Ring_wEmpty : wEmpty Ring
  | Ring_Diff : Diff Ring
  | Ring_Union : Union Ring.

Inductive Algebra : (U Prop) Prop :=
  | Algebra_Gen : Incl gen Algebra
  | Algebra_wEmpty : wEmpty Algebra
  | Algebra_Compl : Compl Algebra
  | Algebra_Union : Union Algebra.

Inductive Monotone_class : (U Prop) Prop :=
  | Monotone_class_Gen : Incl gen Monotone_class
  | Monotone_class_Inter_monot_seq : Inter_monot_seq Monotone_class
  | Monotone_class_Union_monot_seq : Union_monot_seq Monotone_class.

Inductive Lsyst : (U Prop) Prop :=
  | Lsyst_Gen : Incl gen Lsyst
  | Lsyst_wFull : wFull Lsyst
  | Lsyst_Compl : Compl Lsyst
  | Lsyst_Union_disj_seq : Union_disj_seq Lsyst.

Inductive Sigma_ring : (U Prop) Prop :=
  | Sigma_ring_Gen : Incl gen Sigma_ring
  | Sigma_ring_wEmpty : wEmpty Sigma_ring
  | Sigma_ring_Diff : Diff Sigma_ring
  | Sigma_ring_Union_seq : Union_seq Sigma_ring.

Inductive Sigma_algebra : (U Prop) Prop :=
  | Sigma_algebra_Gen : Incl gen Sigma_algebra
  | Sigma_algebra_wEmpty : wEmpty Sigma_algebra
  | Sigma_algebra_Compl : Compl Sigma_algebra
  | Sigma_algebra_Union_seq : Union_seq Sigma_algebra.


End Subset_systems_Def1.

Section Subset_systems_Def2.

Context {U : Type}.
Variable P : (U Prop) Prop. Variable A0 : U Prop.
Definition is_Psyst : Prop := Psyst P A0 = P.

Definition is_Semi_ring : Prop :=
  wEmpty P Inter P Part_diff_finite P.

Definition is_Ring : Prop := Ring P = P.

Definition is_Semi_algebra : Prop :=
  wFull P Inter P Part_compl_finite P.

Definition is_Algebra : Prop := Algebra P = P.

Definition is_Monotone_class : Prop := Monotone_class P = P.

Definition is_Lsyst : Prop := Lsyst P = P.

Definition is_Sigma_ring : Prop := Sigma_ring P = P.

Definition is_Sigma_algebra : Prop := Sigma_algebra P = P.

End Subset_systems_Def2.

Global Hint Constructors Psyst : subset_systems.
Global Hint Unfold is_Semi_ring : subset_systems.
Global Hint Constructors Ring : subset_systems.
Global Hint Unfold is_Semi_algebra : subset_systems.
Global Hint Constructors Algebra : subset_systems.
Global Hint Constructors Monotone_class : subset_systems.
Global Hint Constructors Lsyst : subset_systems.
Global Hint Constructors Sigma_ring : subset_systems.
Global Hint Constructors Sigma_algebra : subset_systems.

Section Subset_systems_Facts1.

Context {U : Type}.
Variable P : (U Prop) Prop.
Lemma Psyst_equiv :
   (A0 : U Prop),
    is_Psyst P A0 P A0 Inter P.
Proof.
split.
intros H; rewrite <- H; auto with subset_systems.
intros [H1 H2]; apply Ext; split.
intros H3; induction H3; try easy.
now apply H2.
apply Psyst_Gen.
Qed.

Lemma Ring_equiv :
  is_Ring P wEmpty P Diff P Union P.
Proof.
split.
intros H; rewrite <- H; auto with subset_systems.
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Ring_Gen.
Qed.

Lemma Algebra_equiv :
  is_Algebra P wEmpty P Compl P Union P.
Proof.
split.
intros H; rewrite <- H; auto with subset_systems.
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Algebra_Gen.
Qed.

Lemma Monotone_class_equiv :
  is_Monotone_class P Inter_monot_seq P Union_monot_seq P.
Proof.
split.
intros H; split; rewrite <- H.
apply Monotone_class_Inter_monot_seq.
apply Monotone_class_Union_monot_seq.
intros [H1 H2]; apply Ext; split.
intros H3; induction H3; try easy; [now apply H1 | now apply H2].
apply Monotone_class_Gen.
Qed.

Lemma Lsyst_equiv :
  is_Lsyst P wFull P Compl P Union_disj_seq P.
Proof.
split.
intros H; repeat split; rewrite <- H.
apply Lsyst_wFull.
apply Lsyst_Compl.
apply Lsyst_Union_disj_seq.
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Lsyst_Gen.
Qed.

Lemma Sigma_ring_equiv :
  is_Sigma_ring P wEmpty P Diff P Union_seq P.
Proof.
split.
intros H; repeat split; rewrite <- H.
apply Sigma_ring_wEmpty.
apply Sigma_ring_Diff.
apply Sigma_ring_Union_seq.
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy.
now apply H2.
now apply H3.
apply Sigma_ring_Gen.
Qed.

Lemma Sigma_algebra_equiv :
  is_Sigma_algebra P wEmpty P Compl P Union_seq P.
Proof.
split.
intros H; repeat split; rewrite <- H.
apply Sigma_algebra_wEmpty.
apply Sigma_algebra_Compl.
apply Sigma_algebra_Union_seq.
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Sigma_algebra_Gen.
Qed.

End Subset_systems_Facts1.

Section Subset_systems_Facts2.

Context {U : Type}.
Variable gen0 gen1 : (U Prop) Prop. Variable A0 : U Prop.
Lemma Psyst_lub_alt :
  Incl gen0 (Psyst gen1 A0)
  Incl (Psyst gen0 A0) (Psyst gen1 A0).
Proof.
intros H A HA; induction HA.
now apply H.
apply Psyst_Mem.
now apply Psyst_Inter.
Qed.

Lemma Ring_lub_alt :
  Incl gen0 (Ring gen1)
  Incl (Ring gen0) (Ring gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Ring_wEmpty.
now apply Ring_Diff.
now apply Ring_Union.
Qed.

Lemma Algebra_lub_alt :
  Incl gen0 (Algebra gen1)
  Incl (Algebra gen0) (Algebra gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Algebra_wEmpty.
now apply Algebra_Compl.
now apply Algebra_Union.
Qed.

Lemma Monotone_class_lub_alt :
  Incl gen0 (Monotone_class gen1)
  Incl (Monotone_class gen0) (Monotone_class gen1).
Proof.
intros H A HA; induction HA.
now apply H.
now apply Monotone_class_Inter_monot_seq.
now apply Monotone_class_Union_monot_seq.
Qed.

Lemma Lsyst_lub_alt :
  Incl gen0 (Lsyst gen1)
  Incl (Lsyst gen0) (Lsyst gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Lsyst_wFull.
now apply Lsyst_Compl.
now apply Lsyst_Union_disj_seq.
Qed.

Lemma Sigma_ring_lub_alt :
  Incl gen0 (Sigma_ring gen1)
  Incl (Sigma_ring gen0) (Sigma_ring gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Sigma_ring_wEmpty.
now apply Sigma_ring_Diff.
now apply Sigma_ring_Union_seq.
Qed.

Lemma Sigma_algebra_lub_alt :
  Incl gen0 (Sigma_algebra gen1)
  Incl (Sigma_algebra gen0) (Sigma_algebra gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Sigma_algebra_wEmpty.
now apply Sigma_algebra_Compl.
now apply Sigma_algebra_Union_seq.
Qed.

End Subset_systems_Facts2.

Section Subset_systems_Facts3.

Context {U : Type}.
Variable P : (U Prop) Prop. Variable gen : (U Prop) Prop. Variable A0 : U Prop.
Lemma Psyst_lub :
  is_Psyst P A0 Incl gen P Incl (Psyst gen A0) P.
Proof.
intros H; rewrite <- H; apply Psyst_lub_alt.
Qed.

Lemma Ring_lub :
  is_Ring P Incl gen P Incl (Ring gen) P.
Proof.
intros H; rewrite <- H; apply Ring_lub_alt.
Qed.

Lemma Algebra_lub :
  is_Algebra P Incl gen P Incl (Algebra gen) P.
Proof.
intros H; rewrite <- H; apply Algebra_lub_alt.
Qed.

Lemma Monotone_class_lub :
  is_Monotone_class P Incl gen P Incl (Monotone_class gen) P.
Proof.
intros H; rewrite <- H; apply Monotone_class_lub_alt.
Qed.

Lemma Lsyst_lub :
  is_Lsyst P Incl gen P Incl (Lsyst gen) P.
Proof.
intros H; rewrite <- H; apply Lsyst_lub_alt.
Qed.

Lemma Sigma_ring_lub :
  is_Sigma_ring P Incl gen P Incl (Sigma_ring gen) P.
Proof.
intros H; rewrite <- H; apply Sigma_ring_lub_alt.
Qed.

Lemma Sigma_algebra_lub :
  is_Sigma_algebra P Incl gen P Incl (Sigma_algebra gen) P.
Proof.
intros H; rewrite <- H; apply Sigma_algebra_lub_alt.
Qed.

End Subset_systems_Facts3.

Section Subset_systems_Facts4.

Context {U : Type}.
Variable gen : (U Prop) Prop. Variable A0 : U Prop.
Lemma Psyst_idem :
  is_Psyst (Psyst gen A0) A0.
Proof.
apply Ext_equiv; split; [now apply Psyst_lub_alt | apply Psyst_Gen].
Qed.

Lemma Ring_idem :
  is_Ring (Ring gen).
Proof.
apply Ext_equiv; split; [now apply Ring_lub_alt | apply Ring_Gen].
Qed.

Lemma Algebra_idem :
  is_Algebra (Algebra gen).
Proof.
apply Ext_equiv; split; [now apply Algebra_lub_alt | apply Algebra_Gen].
Qed.

Lemma Monotone_class_idem :
  is_Monotone_class (Monotone_class gen).
Proof.
apply Ext_equiv; split; [now apply Monotone_class_lub_alt | apply Monotone_class_Gen].
Qed.

Lemma Lsyst_idem :
  is_Lsyst (Lsyst gen).
Proof.
apply Ext_equiv; split; [now apply Lsyst_lub_alt | apply Lsyst_Gen].
Qed.

Lemma Sigma_ring_idem :
  is_Sigma_ring (Sigma_ring gen).
Proof.
apply Ext_equiv; split; [now apply Sigma_ring_lub_alt | apply Sigma_ring_Gen].
Qed.

Lemma Sigma_algebra_idem :
  is_Sigma_algebra (Sigma_algebra gen).
Proof.
apply Ext_equiv; split; [now apply Sigma_algebra_lub_alt | apply Sigma_algebra_Gen].
Qed.

Variable gen0 gen1 : (U Prop) Prop.
Lemma Psyst_monot :
  Incl gen0 gen1 Incl (Psyst gen0 A0) (Psyst gen1 A0).
Proof.
intros; apply Psyst_lub_alt, Incl_trans with gen1; [easy | apply Psyst_Gen].
Qed.

Lemma Ring_monot :
  Incl gen0 gen1 Incl (Ring gen0) (Ring gen1).
Proof.
intros; apply Ring_lub_alt, Incl_trans with gen1; [easy | apply Ring_Gen].
Qed.

Lemma Algebra_monot :
  Incl gen0 gen1 Incl (Algebra gen0) (Algebra gen1).
Proof.
intros; apply Algebra_lub_alt, Incl_trans with gen1; [easy | apply Algebra_Gen].
Qed.

Lemma Monotone_class_monot :
  Incl gen0 gen1 Incl (Monotone_class gen0) (Monotone_class gen1).
Proof.
intros; apply Monotone_class_lub_alt, Incl_trans with gen1; [easy | apply Monotone_class_Gen].
Qed.

Lemma Lsyst_monot :
  Incl gen0 gen1 Incl (Lsyst gen0) (Lsyst gen1).
Proof.
intros; apply Lsyst_lub_alt, Incl_trans with gen1; [easy | apply Lsyst_Gen].
Qed.

Lemma Sigma_ring_monot :
  Incl gen0 gen1 Incl (Sigma_ring gen0) (Sigma_ring gen1).
Proof.
intros; apply Sigma_ring_lub_alt, Incl_trans with gen1; [easy | apply Sigma_ring_Gen].
Qed.

Lemma Sigma_algebra_monot :
  Incl gen0 gen1 Incl (Sigma_algebra gen0) (Sigma_algebra gen1).
Proof.
intros; apply Sigma_algebra_lub_alt, Incl_trans with gen1; [easy | apply Sigma_algebra_Gen].
Qed.

Lemma Psyst_ext :
  Incl gen0 (Psyst gen1 A0)
  Incl gen1 (Psyst gen0 A0)
  Psyst gen0 A0 = Psyst gen1 A0.
Proof.
intros; apply Ext_equiv; split; now apply Psyst_lub_alt.
Qed.

Lemma Ring_ext :
  Incl gen0 (Ring gen1)
  Incl gen1 (Ring gen0)
  Ring gen0 = Ring gen1.
Proof.
intros; apply Ext_equiv; split; now apply Ring_lub_alt.
Qed.

Lemma Algebra_ext :
  Incl gen0 (Algebra gen1)
  Incl gen1 (Algebra gen0)
  Algebra gen0 = Algebra gen1.
Proof.
intros; apply Ext_equiv; split; now apply Algebra_lub_alt.
Qed.

Lemma Monotone_class_ext :
  Incl gen0 (Monotone_class gen1)
  Incl gen1 (Monotone_class gen0)
  Monotone_class gen0 = Monotone_class gen1.
Proof.
intros; apply Ext_equiv; split; now apply Monotone_class_lub_alt.
Qed.

Lemma Sigma_ring_ext :
  Incl gen0 (Sigma_ring gen1)
  Incl gen1 (Sigma_ring gen0)
  Sigma_ring gen0 = Sigma_ring gen1.
Proof.
intros; apply Ext_equiv; split; now apply Sigma_ring_lub_alt.
Qed.

Lemma Lsyst_ext :
  Incl gen0 (Lsyst gen1)
  Incl gen1 (Lsyst gen0)
  Lsyst gen0 = Lsyst gen1.
Proof.
intros; apply Ext_equiv; split; now apply Lsyst_lub_alt.
Qed.

Lemma Sigma_algebra_ext :
  Incl gen0 (Sigma_algebra gen1)
  Incl gen1 (Sigma_algebra gen0)
  Sigma_algebra gen0 = Sigma_algebra gen1.
Proof.
intros; apply Ext_equiv; split; now apply Sigma_algebra_lub_alt.
Qed.

End Subset_systems_Facts4.

Section Subset_system_alt_Facts1.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Algebra_equiv_alt :
  Algebra gen = Gen is_Algebra gen.
Proof.
apply Ext_equiv; split; intros A HA.
induction HA.
now apply Gen_ni_gen.
1,2,3: intros SS HSS1 HSS2; rewrite <- HSS1.
apply Algebra_wEmpty.
apply Algebra_Compl; now apply (Algebra_monot gen SS).
apply Algebra_Union; now apply (Algebra_monot gen SS).
apply HA.
apply Algebra_idem.
apply Algebra_Gen.
Qed.

End Subset_system_alt_Facts1.

Section Subset_system_alt_Facts2.

Context {U : Type}.
Lemma is_Algebra_Inter_compat :
  @IInter_compat U is_Algebra.
Proof.
intros Idx HIdx; rewrite Algebra_equiv; repeat split.
intros SS HSS; rewrite <- (HIdx SS HSS); apply Algebra_wEmpty.
intros A HA SS HSS; rewrite <- (HIdx SS HSS).
now apply Algebra_Compl, Algebra_Gen, HA.
intros A B HA HB SS HSS; rewrite <- (HIdx SS HSS).
now apply Algebra_Union; apply Algebra_Gen; [apply HA | apply HB].
Qed.

Variable gen0 gen1 : (U Prop) Prop.
Lemma Algebra_lub_alt_bis :
  Incl gen0 (Algebra gen1)
  Incl (Algebra gen0) (Algebra gen1).
Proof.
intros; rewrite (Algebra_equiv_alt gen0), (Algebra_equiv_alt gen1).
apply (Gen_lub_alt is_Algebra).
apply is_Algebra_Inter_compat.
now rewrite <- Algebra_equiv_alt.
Qed.

End Subset_system_alt_Facts2.

Section Psyst_Facts.

Context {U : Type}.
Variable gen : (U Prop) Prop. Variable A0 : U Prop.
Lemma Psyst_Nonempty :
  Nonempty (Psyst gen A0).
Proof.
A0; apply Psyst_Mem.
Qed.

Lemma Psyst_Inter_finite :
  Inter_finite (Psyst gen A0).
Proof.
apply Inter_finite_equiv, Psyst_Inter.
Qed.

Lemma Psyst_Inter_monot_finite :
  Inter_monot_finite (Psyst gen A0).
Proof.
apply Inter_finite_monot, Psyst_Inter_finite.
Qed.

Lemma Psyst_wEmpty :
  Compl (Psyst gen A0) wEmpty (Psyst gen A0).
Proof.
intros H; apply Nonempty_wEmpty; [easy | apply Psyst_Inter | ].
A0; apply Psyst_Mem.
Qed.

Variable P : (U Prop) Prop.
Lemma is_Psyst_wEmpty :
  is_Psyst P A0 is_Psyst (fun AP A A = emptyset) emptyset.
Proof.
intros H; rewrite Psyst_equiv in *; split.
now right.
now apply Inter_with_empty.
Qed.

End Psyst_Facts.

Section is_Semi_ring_Facts.

Context {U : Type}.
Variable P : (U Prop) Prop.
Lemma is_Semi_ring_wEmpty :
  is_Semi_ring P wEmpty P.
Proof.
now intros [H _].
Qed.

Lemma is_Semi_ring_Inter :
  is_Semi_ring P Inter P.
Proof.
now intros [_ [H _]].
Qed.

Lemma is_Semi_ring_Part_diff_finite :
  is_Semi_ring P Part_diff_finite P.
Proof.
now intros [_ [_ H]].
Qed.

Lemma is_Semi_ring_is_Psyst :
  is_Semi_ring P is_Psyst P emptyset.
Proof.
intros; apply Psyst_equiv; split.
now apply is_Semi_ring_wEmpty.
now apply is_Semi_ring_Inter.
Qed.

Lemma is_Semi_ring_Inter_finite :
  is_Semi_ring P Inter_finite P.
Proof.
intros; rewrite <- is_Semi_ring_is_Psyst; try easy.
apply Psyst_Inter_finite.
Qed.

Lemma is_Semi_ring_Inter_monot_finite :
  is_Semi_ring P Inter_monot_finite P.
Proof.
intros; rewrite <- is_Semi_ring_is_Psyst; try easy.
apply Psyst_Inter_monot_finite.
Qed.

End is_Semi_ring_Facts.

Section Ring_Facts1.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Ring_Inter :
  Inter (Ring gen).
Proof.
apply Diff_Inter, Ring_Diff.
Qed.

Lemma Ring_is_Psyst :
  is_Psyst (Ring gen) emptyset.
Proof.
apply Psyst_equiv; split; try easy.
apply Ring_wEmpty.
apply Ring_Inter.
Qed.

Lemma Ring_Inter_finite :
  Inter_finite (Ring gen).
Proof.
rewrite <- Ring_is_Psyst; apply Psyst_Inter_finite.
Qed.

Lemma Ring_Compl_loc :
  Compl_loc (Ring gen).
Proof.
apply Diff_Compl_loc, Ring_Diff.
Qed.

Lemma Ring_Sym_diff :
  Sym_diff (Ring gen).
Proof.
apply Sym_diff_Diff_equiv; [apply Ring_Union | apply Ring_Diff].
Qed.

Lemma Ring_Union_disj :
  Union_disj (Ring gen).
Proof.
apply Union_Union_disj, Ring_Union.
Qed.

Lemma Ring_Inter_monot_finite :
  Inter_monot_finite (Ring gen).
Proof.
apply Inter_finite_monot, Ring_Inter_finite.
Qed.

Lemma Ring_Union_finite :
  Union_finite (Ring gen).
Proof.
apply Union_finite_equiv, Ring_Union.
Qed.

Lemma Ring_Union_monot_finite :
  Union_monot_finite (Ring gen).
Proof.
apply Union_finite_monot, Ring_Union_finite.
Qed.

Lemma Ring_Union_disj_finite :
  Union_disj_finite (Ring gen).
Proof.
apply Union_finite_disj, Ring_Union_finite.
Qed.

Variable P : (U Prop) Prop.
Lemma Ring_equiv_def :
  is_Ring P
  (Nonempty P wEmpty P)
  (Diff P Union P
   Diff P Union_disj P
   Sym_diff P Inter P
   Compl_loc P Union_disj P Inter P).
Proof.
rewrite Ring_equiv; split.
intros [H1 H2]; repeat split.
now right.
now left.
intros [[H1 | H1] [[H2 H3] | [[H2 H3] | [[H2 H3] | [H2 [H3 H4]]]]]]; repeat split; try easy.
1,2,4,7: apply Nonempty_wEmpty_Diff; try easy.
1,4,9: now apply Sym_diff_Diff.
2,5,6,9: apply Union_disj_Union; try easy.
1,2,3,5,7: now apply Compl_loc_Diff.
1,2: now apply Sym_diff_Union.
Qed.

Lemma is_Psyst_Sym_diff_is_Ring :
   (A0 : U Prop),
    is_Psyst P A0 Sym_diff P is_Ring P.
Proof.
intros A0 H1 H2; rewrite Ring_equiv_def; split.
left; rewrite <- H1; apply Psyst_Nonempty.
right; right; left; split; try easy.
rewrite <- H1; apply Psyst_Inter.
Qed.

End Ring_Facts1.

Section Ring_Facts2.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Incl_Psyst_Ring :
  Incl (Psyst gen emptyset) (Ring gen).
Proof.
rewrite <- Ring_is_Psyst; apply Psyst_monot, Ring_Gen.
Qed.

Lemma Incl_Ring_Psyst :
  let P := Psyst gen emptyset in
  Sym_diff P Incl (Ring gen) P.
Proof.
intros P H1; assert (H2 : is_Ring P).
  apply Ring_equiv; repeat split.
  apply Psyst_Mem.
  apply Sym_diff_Diff; try easy; apply Psyst_Inter.
  apply Sym_diff_Union; try easy; apply Psyst_Inter.
apply Ring_lub; [easy | apply Psyst_Gen].
Qed.

Lemma Ring_Psyst :
  Ring (Psyst gen emptyset) = Ring gen.
Proof.
intros; apply Ext_equiv; split.
now apply Ring_lub_alt, Incl_Psyst_Ring.
apply Ring_monot, Psyst_Gen.
Qed.

End Ring_Facts2.

Section Ring_Facts3.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Hypothesis H : is_Semi_ring gen.


Lemma Explicit_ring_Gen :
  Incl gen (Union_disj_finite_closure gen).
Proof.
intros A HA.
(repeat_1 A), 0; repeat split; try easy.
now rewrite union_finite_0.
apply disj_finite_0.
Qed.

Lemma Explicit_ring_wEmpty :
  wEmpty (Union_disj_finite_closure gen).
Proof.
destruct H as [H1 _].
now apply Explicit_ring_Gen.
Qed.

Lemma Explicit_ring_Diff :
  Diff (Union_disj_finite_closure gen).
Proof.
destruct H as [_ [H2 H3]].
now apply Diff_Union_disj_finite_closure.
Qed.

Lemma Explicit_ring_Union_disj :
  Union_disj (Union_disj_finite_closure gen).
Proof.
apply Union_disj_Union_disj_finite_closure.
Qed.

Lemma Ring_explicit_aux1 :
  Incl (Ring gen) (Union_disj_finite_closure gen).
Proof.
apply Ring_lub.
apply Ring_equiv_def; split.
right; apply Explicit_ring_wEmpty.
right; left; split; [apply Explicit_ring_Diff | apply Explicit_ring_Union_disj].
apply Explicit_ring_Gen.
Qed.

Lemma Ring_explicit_aux2 :
  Incl (Union_finite_closure gen) (Ring gen).
Proof.
intros A [B [N [HB1 HB2]]].
rewrite HB2; apply Ring_Union_finite.
intros; now apply Ring_Gen, HB1.
Qed.

Lemma Ring_explicit_aux :
  Ring gen = Union_disj_finite_closure gen
  Union_disj_finite_closure gen = Union_finite_closure gen.
Proof.
split; apply Ext_equiv; split.
2: apply Incl_trans with (Union_finite_closure gen).
5: apply Incl_trans with (Ring gen).
1,6: apply Ring_explicit_aux1.
1,3: apply Union_finite_closure_Incl.
1,2: apply Ring_explicit_aux2.
Qed.

Lemma Ring_explicit :
  Ring gen = Union_disj_finite_closure gen.
Proof.
apply Ring_explicit_aux.
Qed.

Lemma Ring_explicit_alt :
  Ring gen = Union_finite_closure gen.
Proof.
destruct Ring_explicit_aux as [H1 H2].
now rewrite H1.
Qed.

End Ring_Facts3.

Section Semi_algebra_Facts.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma is_Semi_algebra_equiv_def_Part_diff_finite :
  is_Semi_algebra gen wFull gen Inter gen Part_diff_finite gen.
Proof.
split.
intros [H1 [H2 H3]]; repeat split; try easy.
now apply Part_compl_Part_diff_finite.
intros [H1 [H2 H3]]; repeat split; try easy.
now apply Part_diff_Part_compl_finite.
Qed.

Lemma is_Semi_algebra_equiv_def_Semi_ring :
  is_Semi_algebra gen is_Semi_ring gen wFull gen.
Proof.
rewrite is_Semi_algebra_equiv_def_Part_diff_finite; unfold is_Semi_ring.
repeat split; try easy.
apply wFull_wEmpty_finite; try easy.
now apply Part_diff_Part_compl_finite.
Qed.

Lemma is_Semi_algebra_is_Semi_ring :
  is_Semi_algebra gen is_Semi_ring gen.
Proof.
now rewrite is_Semi_algebra_equiv_def_Semi_ring.
Qed.


End Semi_algebra_Facts.

Global Hint Resolve <- Ring_equiv : subset_systems.
Section Algebra_Facts1.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Algebra_Diff :
  Diff (Algebra gen).
Proof.
apply Union_Diff_equiv; auto with subset_systems.
Qed.

Local Hint Resolve Algebra_Diff : subset_systems.

Lemma Algebra_is_Ring :
  is_Ring (Algebra gen).
Proof.
apply Ring_equiv; auto with subset_systems.
Qed.

Lemma Algebra_Compl_loc :
  Compl_loc (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Compl_loc.
Qed.

Lemma Algebra_Sym_diff :
  Sym_diff (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Sym_diff.
Qed.

Lemma Algebra_Inter :
  Inter (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Inter.
Qed.

Lemma Algebra_Union_disj :
  Union_disj (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_disj.
Qed.

Lemma Algebra_Inter_finite :
  Inter_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Inter_finite.
Qed.

Lemma Algebra_Inter_monot_finite :
  Inter_monot_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Inter_monot_finite.
Qed.

Lemma Algebra_Union_finite :
  Union_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_finite.
Qed.

Lemma Algebra_Union_monot_finite :
  Union_monot_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_monot_finite.
Qed.

Lemma Algebra_Union_disj_finite :
  Union_disj_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_disj_finite.
Qed.

Lemma Algebra_wFull :
  wFull (Algebra gen).
Proof.
apply wFull_wEmpty_equiv.
apply Algebra_Compl.
apply Algebra_wEmpty.
Qed.

Lemma Algebra_Compl_rev :
  Compl_rev (Algebra gen).
Proof.
apply Compl_equiv, Algebra_Compl.
Qed.

Lemma Algebra_is_Psyst :
  is_Psyst (Algebra gen) emptyset.
Proof.
rewrite <- Algebra_is_Ring; apply Ring_is_Psyst.
Qed.

Lemma Algebra_equiv_def :
  is_Algebra gen wFull gen Diff gen.
Proof.
split.
intros H; rewrite <- H; split; [apply Algebra_wFull | apply Algebra_Diff].
intros [H1 H2]; assert (H3 : Compl gen) by now apply Compl_loc_Compl.
rewrite Algebra_equiv; repeat split; try easy.
now apply wFull_wEmpty_equiv.
now apply Union_Diff_equiv.
Qed.

End Algebra_Facts1.

Section Algebra_Facts2.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Incl_Ring_Algebra :
  Incl (Ring gen) (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_lub_alt.
intros A HA; now apply Ring_Gen, Algebra_Gen.
Qed.

Lemma Incl_Psyst_Algebra :
  Incl (Psyst gen emptyset) (Algebra gen).
Proof.
apply Incl_trans with (Ring gen).
apply Incl_Psyst_Ring.
apply Incl_Ring_Algebra.
Qed.

Lemma Upgrade_Ring_is_Algebra :
   (P : (U Prop) Prop),
    is_Ring P
    (wFull P Compl P)
    is_Algebra P.
Proof.
intros P H1 [H2 | H2].
rewrite Algebra_equiv_def; now rewrite Ring_equiv in H1.
rewrite Algebra_equiv; repeat split.
rewrite <- H1; apply Ring_wEmpty.
1,2: now rewrite Ring_equiv in H1.
Qed.

Lemma Algebra_of_Ring :
  Algebra (Ring gen) = Algebra gen.
Proof.
apply Ext_equiv; split.
rewrite <- (Algebra_idem gen).
apply Algebra_monot, Incl_Ring_Algebra.
apply Algebra_monot, Ring_Gen.
Qed.

Lemma Upgrade_Ring_Algebra :
  (wFull (Ring gen) Compl (Ring gen))
  Ring gen = Algebra gen.
Proof.
intros H.
generalize (Upgrade_Ring_is_Algebra (Ring gen)); intros H3.
rewrite <- H3; try easy.
apply Algebra_of_Ring.
apply Ring_idem.
Qed.

Lemma Incl_Algebra_Psyst :
  let P := Psyst gen emptyset in
  Compl P Incl (Algebra gen) P.
Proof.
intros P H1; assert (H2 : is_Algebra P).
  apply Algebra_equiv; repeat split; try easy.
  now apply Psyst_wEmpty.
  apply Union_Inter_equiv; [easy | apply Psyst_Inter].
apply Algebra_lub; [easy | apply Psyst_Gen].
Qed.

Lemma Algebra_Psyst :
  Algebra (Psyst gen emptyset) = Algebra gen.
Proof.
apply Ext_equiv; split.
now apply Algebra_lub_alt, Incl_Psyst_Algebra.
apply Algebra_monot, Psyst_Gen.
Qed.

End Algebra_Facts2.

Section Algebra_Facts3.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Hypothesis H : is_Semi_algebra gen.

Lemma Algebra_explicit_aux :
  Algebra gen = Union_disj_finite_closure gen
  Union_disj_finite_closure gen = Union_finite_closure gen.
Proof.
rewrite is_Semi_algebra_equiv_def_Semi_ring in H.
destruct H as [H1 H2]; clear H.
destruct (Ring_explicit_aux gen H1) as [H3 H4].
split; try easy; clear H4.
rewrite <- H3; symmetry; rewrite Upgrade_Ring_Algebra; try easy.
left; now apply Ring_Gen.
Qed.

Lemma Algebra_explicit :
  Algebra gen = Union_disj_finite_closure gen.
Proof.
apply Algebra_explicit_aux.
Qed.

Lemma Algebra_explicit_alt :
  Algebra gen = Union_finite_closure gen.
Proof.
destruct Algebra_explicit_aux as [H1 H2].
now rewrite H1.
Qed.

End Algebra_Facts3.

Section Monotone_class_Facts1.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Monotone_class_Inter_monot_finite :
  Inter_monot_finite (Monotone_class gen).
Proof.
apply Inter_monot_seq_finite, Monotone_class_Inter_monot_seq.
Qed.

Lemma Monotone_class_Union_monot_finite :
  Union_monot_finite (Monotone_class gen).
Proof.
apply Union_monot_seq_finite, Monotone_class_Union_monot_seq.
Qed.

End Monotone_class_Facts1.

Section Monotone_class_Facts2.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Hypothesis H : Diff gen.

Definition Monotone_class_diff : (U Prop) (U Prop) Prop :=
  fun A BMonotone_class gen (diff A B) Monotone_class gen (diff B A).

Lemma Monotone_class_diff_sym :
   (A B : U Prop),
    Monotone_class gen B Monotone_class_diff B A Monotone_class_diff A B.
Proof.
intros A B HB [H1 H2]; now split.
Qed.

Lemma Monotone_class_diff_is_Monotone_class :
   (A : U Prop), is_Monotone_class (Monotone_class_diff A).
Proof.
intros A; apply Monotone_class_equiv; split; intros B HB1 HB2; split.
rewrite diff_inter_seq_r; apply Monotone_class_Union_monot_seq.
now apply diff_decr_seq_compat_l.
intros n; now destruct (HB2 n).
rewrite diff_inter_seq_distr_l; apply Monotone_class_Inter_monot_seq.
now apply diff_decr_seq_compat_r.
intros n; now destruct (HB2 n).
rewrite diff_union_seq_r; apply Monotone_class_Inter_monot_seq.
now apply diff_incr_seq_compat_l.
intros n; now destruct (HB2 n).
rewrite diff_union_seq_distr_l; apply Monotone_class_Union_monot_seq.
now apply diff_incr_seq_compat_r.
intros n; now destruct (HB2 n).
Qed.

Lemma Diff_Monotone_class_aux1 :
   A, gen A Incl (Monotone_class gen) (Monotone_class_diff A).
Proof.
intros; apply Monotone_class_lub.
apply Monotone_class_diff_is_Monotone_class.
intros B HB; split; apply Monotone_class_Gen; now apply H.
Qed.

Lemma Diff_Monotone_class_aux2 :
   A,
    Monotone_class gen A
    Incl (Monotone_class gen) (Monotone_class_diff A).
Proof.
intros; apply Monotone_class_lub.
apply Monotone_class_diff_is_Monotone_class.
intros B HB; apply Monotone_class_diff_sym.
now apply Monotone_class_Gen.
now apply Diff_Monotone_class_aux1.
Qed.

Lemma Diff_Monotone_class :
  Diff (Monotone_class gen).
Proof.
intros A B HA HB; now apply Diff_Monotone_class_aux2.
Qed.

End Monotone_class_Facts2.

Section Lsyst_Facts1.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Lsyst_wEmpty :
  wEmpty (Lsyst gen).
Proof.
apply wFull_wEmpty_equiv.
apply Lsyst_Compl.
apply Lsyst_wFull.
Qed.

Lemma Lsyst_Compl_loc :
  Compl_loc (Lsyst gen).
Proof.
apply Union_disj_seq_Compl_loc.
apply Lsyst_wFull.
apply Lsyst_Compl.
apply Lsyst_Union_disj_seq.
Qed.

Lemma Lsyst_Union_monot_seq :
  Union_monot_seq (Lsyst gen).
Proof.
apply Union_disj_monot_seq.
apply Lsyst_Compl_loc.
apply Lsyst_Union_disj_seq.
Qed.

Lemma Lsyst_Inter_monot_seq :
  Inter_monot_seq (Lsyst gen).
Proof.
apply Union_Inter_monot_seq_equiv.
apply Lsyst_Compl.
apply Lsyst_Union_monot_seq.
Qed.

Lemma Lsyst_is_Monotone_class :
  is_Monotone_class (Lsyst gen).
Proof.
apply Monotone_class_equiv; split.
apply Lsyst_Inter_monot_seq.
apply Lsyst_Union_monot_seq.
Qed.

Lemma Lsyst_Union_monot_finite :
  Union_monot_finite (Lsyst gen).
Proof.
rewrite <- Lsyst_is_Monotone_class; apply Monotone_class_Union_monot_finite.
Qed.

Lemma Lsyst_Inter_monot_finite :
  Inter_monot_finite (Lsyst gen).
Proof.
rewrite <- Lsyst_is_Monotone_class; apply Monotone_class_Inter_monot_finite.
Qed.

Lemma Lsyst_Compl_rev :
  Compl_rev (Lsyst gen).
Proof.
apply Compl_equiv, Lsyst_Compl.
Qed.

Lemma Lsyst_Union_disj_finite :
  Union_disj_finite (Lsyst gen).
Proof.
apply Union_disj_seq_finite.
apply Lsyst_wEmpty.
apply Lsyst_Union_disj_seq.
Qed.

Lemma Lsyst_Union_disj :
  Union_disj (Lsyst gen).
Proof.
apply Union_disj_finite_equiv, Lsyst_Union_disj_finite.
Qed.

Lemma Lsyst_equiv_def :
  is_Lsyst gen wFull gen Compl_loc gen Union_monot_seq gen.
Proof.
split.
intros H; rewrite <- H; repeat split;
    [apply Lsyst_wFull | apply Lsyst_Compl_loc | apply Lsyst_Union_monot_seq].
intros [H1 [H2 H3]]; assert (H4 : Compl gen) by now apply Compl_loc_Compl.
rewrite Lsyst_equiv; repeat split; try easy.
now apply Union_monot_disj_seq_alt.
Qed.

End Lsyst_Facts1.

Section Lsyst_Facts2.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Incl_Monotone_class_Lsyst :
  Incl (Monotone_class gen) (Lsyst gen).
Proof.
rewrite <- Lsyst_is_Monotone_class; apply Monotone_class_lub_alt.
intros A HA; now apply Monotone_class_Gen, Lsyst_Gen.
Qed.

Lemma Incl_Lsyst_Monotone_class_aux :
  wFull (Monotone_class gen) Compl (Monotone_class gen)
  Union_disj_seq (Monotone_class gen)
  Incl (Lsyst gen) (Monotone_class gen).
Proof.
intros H1 H2 H3; assert (H4 : is_Lsyst (Monotone_class gen)) by now apply Lsyst_equiv.
apply Lsyst_lub; [easy | apply Monotone_class_Gen].
Qed.

Lemma Incl_Lsyst_Monotone_class :
  wFull (Monotone_class gen) Compl_loc (Monotone_class gen)
  Incl (Lsyst gen) (Monotone_class gen).
Proof.
intros H1 H2; assert (H3 : Compl (Monotone_class gen)) by now apply Compl_loc_Compl.
apply Incl_Lsyst_Monotone_class_aux; try easy.
apply Union_monot_disj_seq_alt; try easy; apply Monotone_class_Union_monot_seq.
Qed.

Lemma Lsyst_Monotone_class :
  Lsyst (Monotone_class gen) = Lsyst gen.
Proof.
apply Ext_equiv; split.
apply Lsyst_lub_alt, Incl_Monotone_class_Lsyst.
apply Lsyst_monot, Monotone_class_Gen.
Qed.

End Lsyst_Facts2.

Section Lsyst_Facts3.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Hypothesis H : Inter gen.

Definition Lsyst_inter : (U Prop) (U Prop) Prop :=
  fun A BLsyst gen B Lsyst gen (inter A B).

Lemma Lsyst_inter_sym :
   (A B : U Prop),
    Lsyst gen A Lsyst_inter A B Lsyst_inter B A.
Proof.
intros A B HA [H1 H2]; now rewrite inter_comm in H2.
Qed.

Lemma Lsyst_inter_is_Lsyst :
   (A : U Prop), Lsyst gen A is_Lsyst (Lsyst_inter A).
Proof.
intros A HA; apply Lsyst_equiv_def; split; [ | split].
split; [apply Lsyst_wFull | now rewrite inter_full_r].
intros B C HBC [HB1 HB2] [HC1 HC2]; split.
now apply Lsyst_Compl_loc.
rewrite inter_diff_distr_l; apply Lsyst_Compl_loc;
    try easy; now apply inter_monot_r.
intros B HB1 HB2; split.
apply Lsyst_Union_monot_seq; try easy; intros n; now destruct (HB2 n).
rewrite inter_union_seq_distr_l; apply Lsyst_Union_monot_seq.
now apply inter_incr_seq_compat_l.
intros; apply HB2.
Qed.

Lemma Inter_Lsyst_aux1 :
   (A : U Prop), gen A Incl (Lsyst gen) (Lsyst_inter A).
Proof.
intros; apply Lsyst_lub.
apply Lsyst_inter_is_Lsyst; now apply Lsyst_Gen.
intros B HB; split; apply Lsyst_Gen; [easy | now apply H].
Qed.

Lemma Inter_Lsyst_aux2 :
   A, Lsyst gen A Incl (Lsyst gen) (Lsyst_inter A).
Proof.
intros; apply Lsyst_lub.
now apply Lsyst_inter_is_Lsyst.
intros B HB; apply Lsyst_inter_sym; try easy.
now apply Lsyst_Gen.
now apply Inter_Lsyst_aux1.
Qed.

Lemma Inter_Lsyst :
  Inter (Lsyst gen).
Proof.
intros A B HA HB; now apply Inter_Lsyst_aux2.
Qed.

End Lsyst_Facts3.


Section Sigma_algebra_Facts1.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Sigma_algebra_Union :
  Union (Sigma_algebra gen).
Proof.
apply Union_seq_Union, Sigma_algebra_Union_seq.
Qed.

Lemma Sigma_algebra_is_Algebra :
  is_Algebra (Sigma_algebra gen).
Proof.
apply Algebra_equiv; repeat split.
apply Sigma_algebra_wEmpty.
apply Sigma_algebra_Compl.
apply Sigma_algebra_Union.
Qed.

Lemma Sigma_algebra_wFull :
  wFull (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_wFull.
Qed.

Lemma Sigma_algebra_Compl_rev :
  Compl_rev (Sigma_algebra gen).
Proof.
apply Compl_equiv, Sigma_algebra_Compl.
Qed.

Lemma Sigma_algebra_Compl_loc :
  Compl_loc (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Compl_loc.
Qed.

Lemma Sigma_algebra_Diff :
  Diff (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Diff.
Qed.

Lemma Sigma_algebra_Sym_diff :
  Sym_diff (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Sym_diff.
Qed.

Lemma Sigma_algebra_Inter :
  Inter (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Inter.
Qed.

Lemma Sigma_algebra_Union_disj :
  Union_disj (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Union_disj.
Qed.

Lemma Sigma_algebra_Inter_finite :
  Inter_finite (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Inter_finite.
Qed.

Lemma Sigma_algebra_Inter_monot_finite :
  Inter_monot_finite (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Inter_monot_finite.
Qed.

Lemma Sigma_algebra_Union_finite :
  Union_finite (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Union_finite.
Qed.

Lemma Sigma_algebra_Union_monot_finite :
  Union_monot_finite (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Union_monot_finite.
Qed.

Lemma Sigma_algebra_Union_disj_finite :
  Union_disj_finite (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Union_disj_finite.
Qed.

Lemma Sigma_algebra_Inter_seq :
  Inter_seq (Sigma_algebra gen).
Proof.
apply Union_Inter_seq_equiv.
apply Sigma_algebra_Compl.
apply Sigma_algebra_Union_seq.
Qed.

Lemma Sigma_algebra_Inter_monot_seq :
  Inter_monot_seq (Sigma_algebra gen).
Proof.
apply Inter_seq_monot, Sigma_algebra_Inter_seq.
Qed.

Lemma Sigma_algebra_Union_monot_seq :
  Union_monot_seq (Sigma_algebra gen).
Proof.
apply Union_seq_monot, Sigma_algebra_Union_seq.
Qed.

Lemma Sigma_algebra_Union_disj_seq :
  Union_disj_seq (Sigma_algebra gen).
Proof.
apply Union_seq_disj, Sigma_algebra_Union_seq.
Qed.

Lemma Sigma_algebra_gen_remove :
   A, Sigma_algebra gen A
    Incl (Sigma_algebra (add gen A)) (Sigma_algebra gen).
Proof.
intros A HA B HB; induction HB as [B [ | HB] | | | ].
now apply Sigma_algebra_Gen.
now rewrite HB.
apply Sigma_algebra_wEmpty.
now apply Sigma_algebra_Compl.
now apply Sigma_algebra_Union_seq.
Qed.

Lemma Sigma_algebra_gen_remove_alt :
   A, Sigma_algebra gen A Incl (add gen A) (Sigma_algebra gen).
Proof.
intros A HA; apply Incl_trans with (2 := Sigma_algebra_gen_remove _ HA).
apply Sigma_algebra_Gen.
Qed.

Lemma Sigma_algebra_gen_remove_full :
  Incl (add gen fullset) (Sigma_algebra gen).
Proof.
apply Sigma_algebra_gen_remove_alt, Sigma_algebra_wFull.
Qed.

Lemma Sigma_algebra_gen_add_eq :
   A, Sigma_algebra gen A Sigma_algebra (add gen A) = Sigma_algebra gen.
Proof.
intros; apply Ext_equiv; split.
now apply Sigma_algebra_gen_remove.
apply Sigma_algebra_monot, incl_add_r.
Qed.

End Sigma_algebra_Facts1.

Section Sigma_algebra_Facts2.

Context {U1 U2 : Type}. Variable genU1 : (U1 Prop) Prop. Variable genU2 : (U2 Prop) Prop.
Variable f : U1 U2.

Lemma is_Sigma_algebra_Image : is_Sigma_algebra (Image f (Sigma_algebra genU1)).
Proof.
apply Sigma_algebra_equiv; repeat split.
apply Sigma_algebra_wEmpty.
intros A2 HA2; apply Sigma_algebra_Compl; easy.
intros A2 HA2; apply Sigma_algebra_Union_seq; easy.
Qed.

Lemma is_Sigma_algebra_Preimage :
  is_Sigma_algebra (Preimage f (Sigma_algebra genU2)).
Proof.
apply Sigma_algebra_equiv; repeat split.
unfold wEmpty; rewrite <- (preimage_emptyset f).
apply Im, Sigma_algebra_wEmpty.
intros A1 [A2 HA2]; rewrite <- preimage_compl.
apply Im, Sigma_algebra_Compl; easy.
intros A1 HA1; unfold Preimage in *; rewrite image_eq in HA1.
destruct (choice (fun n A2
    Sigma_algebra genU2 A2 A1 n = preimage f A2) HA1) as [A2 HA2].
assert (H : union_seq A1 = preimage f (union_seq A2)).
  rewrite preimage_union_seq_distr; f_equal.
  apply subset_seq_ext; intros n; rewrite (proj2 (HA2 n)); easy.
rewrite H; apply Im; apply Sigma_algebra_Union_seq; intro; apply HA2.
Qed.

End Sigma_algebra_Facts2.

Section Sigma_algebra_Facts3.

Context {U1 U2 : Type}. Variable genU1 : (U1 Prop) Prop. Variable genU2 : (U2 Prop) Prop.
Variable f : U1 U2.

Lemma Sigma_algebra_Preimage :
  Sigma_algebra (Preimage f genU2) = Preimage f (Sigma_algebra genU2).
Proof.
apply Ext_equiv; split.
rewrite <- is_Sigma_algebra_Preimage.
apply Sigma_algebra_monot, Preimage_monot, Sigma_algebra_Gen.
apply Incl_Image_Preimage_Incl, Sigma_algebra_lub.
apply is_Sigma_algebra_Image.
apply Preimage_Incl_Incl_Image, Sigma_algebra_Gen.
Qed.

End Sigma_algebra_Facts3.

Section Sigma_algebra_Facts4.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Sigma_algebra_is_Psyst :
  is_Psyst (Sigma_algebra gen) emptyset.
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_is_Psyst.
Qed.

Lemma Incl_Psyst_Sigma_algebra :
  Incl (Psyst gen emptyset) (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Psyst; apply Psyst_lub_alt.
intros A HA; now apply Psyst_Gen, Sigma_algebra_Gen.
Qed.

Lemma Incl_Sigma_algebra_Psyst_aux :
  let P := Psyst gen emptyset in
  Compl P Union_seq P
  Incl (Sigma_algebra gen) P.
Proof.
intros P H1 H2; assert (H3 : is_Sigma_algebra P).
  apply Sigma_algebra_equiv; repeat split; try easy.
  now apply Psyst_wEmpty.
apply Sigma_algebra_lub; [easy | apply Psyst_Gen].
Qed.

Lemma Incl_Sigma_algebra_Psyst :
  let P := Psyst gen emptyset in
  Compl P Union_disj_seq P
  Incl (Sigma_algebra gen) P.
Proof.
intros; apply Incl_Sigma_algebra_Psyst_aux; try easy.
apply Union_disj_seq_Union_seq_alt; try easy.
apply Psyst_Inter.
Qed.

Lemma Sigma_algebra_Psyst :
  Sigma_algebra (Psyst gen emptyset) = Sigma_algebra gen.
Proof.
apply Ext_equiv; split.
now apply Sigma_algebra_lub_alt, Incl_Psyst_Sigma_algebra.
apply Sigma_algebra_monot, Psyst_Gen.
Qed.

Lemma Incl_Algebra_Sigma_algebra :
  Incl (Algebra gen) (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Algebra; apply Algebra_lub_alt.
intros A HA; now apply Algebra_Gen, Sigma_algebra_Gen.
Qed.

Lemma Incl_Sigma_algebra_Algebra_aux :
  Union_seq (Algebra gen) Incl (Sigma_algebra gen) (Algebra gen).
Proof.
intros H1; assert (H2 : is_Sigma_algebra (Algebra gen)).
  apply Sigma_algebra_equiv; repeat split; try easy.
  apply Algebra_wEmpty.
  apply Algebra_Compl.
apply Sigma_algebra_lub; [easy | apply Algebra_Gen].
Qed.

Lemma Incl_Sigma_algebra_Algebra :
  Union_monot_seq (Algebra gen) Incl (Sigma_algebra gen) (Algebra gen).
Proof.
intros; apply Incl_Sigma_algebra_Algebra_aux,
    Union_monot_seq_Union_seq_alt; try easy.
apply Algebra_Compl.
apply Algebra_Union.
Qed.

Lemma Sigma_algebra_Algebra :
  Sigma_algebra (Algebra gen) = Sigma_algebra gen.
Proof.
apply Ext_equiv; split.
apply Sigma_algebra_lub_alt, Incl_Algebra_Sigma_algebra.
apply Sigma_algebra_monot, Algebra_Gen.
Qed.

Lemma Sigma_algebra_is_Monotone_class :
  is_Monotone_class (Sigma_algebra gen).
Proof.
apply Monotone_class_equiv; split.
apply Sigma_algebra_Inter_monot_seq.
apply Sigma_algebra_Union_monot_seq.
Qed.

Lemma Incl_Monotone_class_Sigma_algebra :
  Incl (Monotone_class gen) (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Monotone_class; apply Monotone_class_lub_alt.
intros A HA; now apply Monotone_class_Gen, Sigma_algebra_Gen.
Qed.

Lemma Incl_Sigma_algebra_Monotone_class_aux :
  wEmpty (Monotone_class gen) Compl (Monotone_class gen)
  Union_seq (Monotone_class gen)
  Incl (Sigma_algebra gen) (Monotone_class gen).
Proof.
intros H1 H2 H3; assert (H4 : is_Sigma_algebra (Monotone_class gen)).
  apply Sigma_algebra_equiv; now repeat split.
apply Sigma_algebra_lub; [easy | apply Monotone_class_Gen].
Qed.

Lemma Incl_Sigma_algebra_Monotone_class :
  wEmpty (Monotone_class gen) Compl (Monotone_class gen)
  Union (Monotone_class gen)
  Incl (Sigma_algebra gen) (Monotone_class gen).
Proof.
intros; apply Incl_Sigma_algebra_Monotone_class_aux; try easy.
apply Union_monot_seq_Union_seq_alt; try easy.
apply Monotone_class_Union_monot_seq.
Qed.

Lemma Sigma_algebra_Monotone_class :
  Sigma_algebra (Monotone_class gen) = Sigma_algebra gen.
Proof.
apply Ext_equiv; split.
apply Sigma_algebra_lub_alt, Incl_Monotone_class_Sigma_algebra.
apply Sigma_algebra_monot, Monotone_class_Gen.
Qed.

Lemma Sigma_algebra_is_Lsyst :
  is_Lsyst (Sigma_algebra gen).
Proof.
apply Lsyst_equiv; repeat split.
apply Sigma_algebra_wFull.
apply Sigma_algebra_Compl.
apply Sigma_algebra_Union_disj_seq.
Qed.

Lemma Incl_Lsyst_Sigma_algebra :
  Incl (Lsyst gen) (Sigma_algebra gen).
Proof.
rewrite <- Sigma_algebra_is_Lsyst; apply Lsyst_lub_alt.
intros A HA; now apply Lsyst_Gen, Sigma_algebra_Gen.
Qed.

Lemma Incl_Sigma_algebra_Lsyst_aux :
  Union_seq (Lsyst gen)
  Incl (Sigma_algebra gen) (Lsyst gen).
Proof.
intros H1; assert (H2 : is_Sigma_algebra (Lsyst gen)).
  apply Sigma_algebra_equiv; repeat split; try easy.
  apply Lsyst_wEmpty.
  apply Lsyst_Compl.
apply Sigma_algebra_lub; [easy | apply Lsyst_Gen].
Qed.

Lemma Incl_Sigma_algebra_Lsyst :
  Inter (Lsyst gen)
  Incl (Sigma_algebra gen) (Lsyst gen).
Proof.
intros; apply Incl_Sigma_algebra_Lsyst_aux.
apply Union_disj_seq_Union_seq_alt; try easy.
apply Lsyst_Compl.
apply Lsyst_Union_disj_seq.
Qed.

Lemma Sigma_algebra_Lsyst :
  Sigma_algebra (Lsyst gen) = Sigma_algebra gen.
Proof.
apply Ext_equiv; split.
apply Sigma_algebra_lub_alt, Incl_Lsyst_Sigma_algebra.
apply Sigma_algebra_monot, Lsyst_Gen.
Qed.

Lemma Psyst_Lsyst_is_Sigma_algebra :
   (A0 : U Prop),
    is_Psyst gen A0 is_Lsyst gen is_Sigma_algebra gen.
Proof.
intros A0 H1 H2; unfold is_Sigma_algebra.
rewrite <- H2 at 2; rewrite Psyst_equiv in H1.
apply Ext_equiv; split.
apply Incl_Sigma_algebra_Lsyst; now rewrite H2.
apply Incl_Lsyst_Sigma_algebra.
Qed.

Lemma Algebra_Monotone_class_is_Sigma_algebra :
  is_Algebra gen is_Monotone_class gen is_Sigma_algebra gen.
Proof.
intros H1 H2; unfold is_Sigma_algebra.
rewrite <- H2 at 2; rewrite Algebra_equiv in H1.
apply Ext_equiv; split.
apply Incl_Sigma_algebra_Monotone_class; now rewrite H2.
apply Incl_Monotone_class_Sigma_algebra.
Qed.

End Sigma_algebra_Facts4.

Section Dynkin_pi_lambda_Theorem.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Lsyst_Psyst_Inter :
   (A0 : U Prop),
    Inter (Lsyst (Psyst gen A0)).
Proof.
intros; apply Inter_Lsyst, Psyst_Inter.
Qed.

Lemma Lsyst_Psyst_is_Psyst :
   (A0 : U Prop),
    is_Psyst (Lsyst (Psyst gen A0)) A0.
Proof.
intros; apply Psyst_equiv; split.
apply Lsyst_Gen, Psyst_Mem.
apply Lsyst_Psyst_Inter.
Qed.

Theorem Dynkin_pi_lambda :
   (A0 : U Prop),
    Sigma_algebra (Psyst gen A0) = Lsyst (Psyst gen A0).
Proof.
intros A0; rewrite <- Sigma_algebra_Lsyst.
apply (Psyst_Lsyst_is_Sigma_algebra _ A0).
apply Lsyst_Psyst_is_Psyst.
apply Lsyst_idem.
Qed.

Theorem Dynkin_pi_lambda_Prop :
   (P : (U Prop) Prop) (A0 : U Prop),
    is_Lsyst P
    Incl (Psyst gen A0) P Incl (Sigma_algebra gen) P.
Proof.
intros P A0 H1 H2; rewrite <- H1.
apply Incl_trans with (Sigma_algebra (Psyst gen A0)).
apply Sigma_algebra_monot, Psyst_Gen.
rewrite Dynkin_pi_lambda.
now apply Lsyst_monot.
Qed.

End Dynkin_pi_lambda_Theorem.

Section Monotone_class_Theorem.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Monotone_class_Algebra_wFull :
  wFull (Monotone_class (Algebra gen)).
Proof.
apply Monotone_class_Gen, Algebra_wFull.
Qed.

Lemma Monotone_class_Algebra_Diff :
  Diff (Monotone_class (Algebra gen)).
Proof.
apply Diff_Monotone_class, Algebra_Diff.
Qed.

Lemma Monotone_class_Algebra_is_Algebra :
  is_Algebra (Monotone_class (Algebra gen)).
Proof.
apply Algebra_equiv_def; repeat split.
apply Monotone_class_Algebra_wFull.
apply Monotone_class_Algebra_Diff.
Qed.

Theorem monotone_class :
  Sigma_algebra (Algebra gen) = Monotone_class (Algebra gen).
Proof.
rewrite <- Sigma_algebra_Monotone_class.
apply Algebra_Monotone_class_is_Sigma_algebra.
apply Monotone_class_Algebra_is_Algebra.
apply Monotone_class_idem.
Qed.

Theorem monotone_class_Prop :
   (P : (U Prop) Prop),
    is_Monotone_class P
    Incl (Algebra gen) P Incl (Sigma_algebra gen) P.
Proof.
intros P H1 H2; rewrite <- H1.
apply Incl_trans with (Sigma_algebra (Algebra gen)).
apply Sigma_algebra_monot, Algebra_Gen.
rewrite monotone_class.
now apply Monotone_class_monot.
Qed.

End Monotone_class_Theorem.

Section Gen_Prod_Def0.

Context {U1 U2 : Type}.
Variable genU1 : (U1 Prop) Prop. Variable genU2 : (U2 Prop) Prop.
Definition Prod_Sigma_algebra : (U1 × U2 Prop) Prop :=
  Prod (Sigma_algebra genU1) (Sigma_algebra genU2).

Definition Sigma_algebra_Prod : (U1 × U2 Prop) Prop :=
  Sigma_algebra Prod_Sigma_algebra.

Definition Gen_Prod : (U1 × U2 Prop) Prop :=
  Prod (add genU1 fullset) (add genU2 fullset).

End Gen_Prod_Def0.

Section Gen_Prod_Def1.

Context {U : Type}.
Variable genU : (U Prop) Prop.
Definition Gen_Prod_diag : (U × U Prop) Prop := Gen_Prod genU genU.

End Gen_Prod_Def1.

Section Prod_Sigma_algebra_Facts1.

Context {U1 U2 : Type}. Variable genU1 : (U1 Prop) Prop. Variable genU2 : (U2 Prop) Prop.
Let genU1xU2 := Gen_Prod genU1 genU2.

Lemma Sigma_algebra_prod_alt :
   A1 A2, Sigma_algebra genU1 A1 Sigma_algebra genU2 A2
    Sigma_algebra_Prod genU1 genU2 (prod A1 A2).
Proof.
intros; apply Sigma_algebra_Gen; now A1, A2.
Qed.

Lemma Sigma_algebra_prod_full_r :
   A1, Sigma_algebra genU1 A1 Sigma_algebra genU1xU2 (prod A1 fullset).
Proof.
intros A1 HA1; induction HA1 as [A1 HA1 | | | ].
apply Sigma_algebra_Gen; A1, fullset; repeat split;
    [now apply incl_add_r | apply add_in].
rewrite prod_empty_l; apply Sigma_algebra_wEmpty.
rewrite prod_compl_full; now apply Sigma_algebra_Compl.
rewrite prod_union_seq_full; now apply Sigma_algebra_Union_seq.
Qed.

Lemma Sigma_algebra_prod_full_l :
   A2, Sigma_algebra genU2 A2 Sigma_algebra genU1xU2 (prod fullset A2).
Proof.
intros A2 HA2; induction HA2 as [A2 HA2 | | | ].
apply Sigma_algebra_Gen; fullset, A2; repeat split;
    [apply add_in | now apply incl_add_r].
rewrite prod_empty_r; apply Sigma_algebra_wEmpty.
rewrite prod_full_compl; now apply Sigma_algebra_Compl.
rewrite prod_full_union_seq; now apply Sigma_algebra_Union_seq.
Qed.

Lemma Sigma_algebra_prod :
   A1 A2, Sigma_algebra genU1 A1 Sigma_algebra genU2 A2
    Sigma_algebra genU1xU2 (prod A1 A2).
Proof.
intros; rewrite prod_equiv; apply Sigma_algebra_Inter.
now apply Sigma_algebra_prod_full_r.
now apply Sigma_algebra_prod_full_l.
Qed.

Lemma Gen_Prod_is_Prod_Sigma_algebra :
  Incl genU1xU2 (Prod_Sigma_algebra genU1 genU2).
Proof.
apply Prod_monot;
    (apply incl_add_l; split;
    [apply Sigma_algebra_Gen | apply Sigma_algebra_wFull]).
Qed.

Lemma Sigma_algebra_Prod_eq :
   Sigma_algebra_Prod genU1 genU2 = Sigma_algebra genU1xU2.
Proof.
apply Sigma_algebra_ext.
intros A [A1 [A2 [HA1 [HA2 HA]]]]; rewrite HA; now apply Sigma_algebra_prod.
apply Incl_trans with (2 := Sigma_algebra_Gen _), Gen_Prod_is_Prod_Sigma_algebra.
Qed.

End Prod_Sigma_algebra_Facts1.

Section Prod_Sigma_algebra_Facts2.

Context {U1 U2 : Type}. Variable genU1 : (U1 Prop) Prop. Variable genU2 : (U2 Prop) Prop.
Let genU1xU2 := Gen_Prod genU1 genU2.
Let genU2xU1 := Gen_Prod genU2 genU1.

Lemma Sigma_algebra_swap_c :
   A, Sigma_algebra genU1xU2 A Sigma_algebra genU2xU1 (swap_c A).
Proof.
intros A HA; induction HA as [A [A1 [A2 [HA1 [HA2 HA]]]] | | | ].
rewrite HA, swap_c_prod.
apply Sigma_algebra_prod;
    now apply Sigma_algebra_gen_remove_alt with (1 := Sigma_algebra_wFull _).
apply Sigma_algebra_wEmpty.
now apply Sigma_algebra_Compl.
now apply Sigma_algebra_Union_seq.
Qed.

End Prod_Sigma_algebra_Facts2.

Section Prod_Sigma_algebra_Facts3.

Context {U1 U2 : Type}. Variable genU1 : (U1 Prop) Prop. Variable genU2 : (U2 Prop) Prop.
Let genU1xU2 := Gen_Prod genU1 genU2.
Let genU2xU1 := Gen_Prod genU2 genU1.

Lemma Sigma_algebra_swap_c_rev :
   A, Sigma_algebra genU2xU1 (swap_c A) Sigma_algebra genU1xU2 A.
Proof.
intros; rewrite <- swap_c_invol; now apply Sigma_algebra_swap_c.
Qed.

Lemma Sigma_algebra_swap_c_equiv :
   A, Sigma_algebra genU1xU2 A Sigma_algebra genU2xU1 (swap_c A).
Proof.
intros; split; [apply Sigma_algebra_swap_c | apply Sigma_algebra_swap_c_rev].
Qed.

End Prod_Sigma_algebra_Facts3.

Section Prod_Sigma_algebra_Facts4.

Context {U V : Type}. Variable genU1 genU2 : (U Prop) Prop. Variable genV1 genV2 : (V Prop) Prop.
Let genU1xU2 := Gen_Prod genU1 genV1.
Let genV1xV2 := Gen_Prod genU2 genV2.

Lemma Sigma_algebra_Gen_Prod_ext_aux :
  Sigma_algebra genU1 = Sigma_algebra genU2
  Sigma_algebra genV1 = Sigma_algebra genV2
  Incl genU1xU2 (Sigma_algebra genV1xV2).
Proof.
intros H1 H2 A [A1 [A2 [HA1 [HA2 HA]]]]; rewrite HA.
apply Sigma_algebra_prod; [rewrite <- H1 | rewrite <- H2];
    now apply Sigma_algebra_gen_remove_full.
Qed.

End Prod_Sigma_algebra_Facts4.

Section Prod_Sigma_algebra_Facts5.

Context {U V : Type}. Variable genU1 genU2 : (U Prop) Prop. Variable genV1 genV2 : (V Prop) Prop.
Let genU1xU2 := Gen_Prod genU1 genV1.
Let genV1xV2 := Gen_Prod genU2 genV2.

Lemma Sigma_algebra_Gen_Prod_ext :
  Sigma_algebra genU1 = Sigma_algebra genU2
  Sigma_algebra genV1 = Sigma_algebra genV2
  Sigma_algebra genU1xU2 = Sigma_algebra genV1xV2.
Proof.
intros; apply Ext_equiv; split;
    now apply Sigma_algebra_lub_alt, Sigma_algebra_Gen_Prod_ext_aux.
Qed.

End Prod_Sigma_algebra_Facts5.

Section Algebra_Facts4.

Context {U1 U2 : Type}.
Variable genU1 : (U1 Prop) Prop. Variable genU2 : (U2 Prop) Prop.
Lemma Prod_Sigma_algebra_wFull :
  wFull (Prod_Sigma_algebra genU1 genU2).
Proof.
fullset, fullset; repeat split; try apply Sigma_algebra_wFull.
now rewrite prod_full.
Qed.

Lemma Prod_Sigma_algebra_Inter :
  Inter (Prod_Sigma_algebra genU1 genU2).
Proof.
intros A B [A1 [A2 HA]] [B1 [B2 HB]].
(inter A1 B1), (inter A2 B2); repeat split.
1,2: now apply Sigma_algebra_Inter.
destruct HA as [_ [_ HA]]; rewrite HA.
destruct HB as [_ [_ HB]]; rewrite HB.
apply prod_inter.
Qed.

Lemma Prod_Sigma_algebra_Part_compl_finite :
  Part_compl_finite (Prod_Sigma_algebra genU1 genU2).
Proof.
intros A [A1 [A2 HA]].
(fun nmatch n with
  | 0 ⇒ prod (compl A1) A2
  | 1 ⇒ prod fullset (compl A2)
  | _emptyset
  end).
1.
split.
intros n Hn; rewrite lt_2 in Hn; destruct Hn as [Hn | Hn]; rewrite Hn.
(compl A1); A2; repeat split; try easy.
now apply Sigma_algebra_Compl.
fullset; (compl A2); repeat split.
apply Sigma_algebra_wFull.
now apply Sigma_algebra_Compl.
apply partition_finite_1.
destruct HA as [_ [_ HA]]; rewrite HA.
apply prod_compl_partition.
Qed.

Lemma Algebra_product_explicit :
  Algebra (Prod_Sigma_algebra genU1 genU2) =
    Union_disj_finite_closure (Prod_Sigma_algebra genU1 genU2).
Proof.
apply Algebra_explicit; repeat split.
apply Prod_Sigma_algebra_wFull.
apply Prod_Sigma_algebra_Inter.
apply Prod_Sigma_algebra_Part_compl_finite.
Qed.

End Algebra_Facts4.

Section Algebra_Facts5.

Context {U1 U2 : Type}.
Variable genU1 : (U1 Prop) Prop. Variable genU2 : (U2 Prop) Prop.
Lemma Algebra_Gen_Prod_Prod_Sigma_algebra_Incl :
  Incl (Algebra (Gen_Prod genU1 genU2)) (Algebra (Prod_Sigma_algebra genU1 genU2)).
Proof.
apply Algebra_monot, Gen_Prod_is_Prod_Sigma_algebra.
Qed.

End Algebra_Facts5.

Section More_Facts.

Context {U : Type}.
Variable gen : (U Prop) Prop.
Lemma Algebra_Prop : P, Algebra gen (Prop_cst P).
Proof.
intros P; case (classic P); intros.
rewrite (subset_ext (Prop_cst P) fullset); [apply Algebra_wFull | easy].
rewrite (subset_ext (Prop_cst P) emptyset); [apply Algebra_wEmpty | easy].
Qed.

Lemma Lsyst_Prop : P, Lsyst gen (Prop_cst P).
Proof.
intros P; case (classic P); intros.
rewrite (subset_ext (Prop_cst P) fullset); [apply Lsyst_wFull | easy].
rewrite (subset_ext (Prop_cst P) emptyset); [apply Lsyst_wEmpty | easy].
Qed.

Lemma Sigma_algebra_Prop : P, Sigma_algebra gen (Prop_cst P).
Proof.
intros; apply Incl_Algebra_Sigma_algebra, Algebra_Prop.
Qed.

Lemma Sigma_algebra_correct :
   P : ((U Prop) Prop) Prop,
    IIncl is_Sigma_algebra P gen, P (Sigma_algebra gen).
Proof.
intros; split.
intros HP gen'; apply HP, Sigma_algebra_idem.
intros HP calS HcalS; rewrite <- HcalS; apply HP.
Qed.

Definition trivial_SA := pair (@emptyset U) fullset.

Lemma is_Sigma_algebra_trivial_SA : is_Sigma_algebra trivial_SA.
Proof.
apply Ext_equiv; split; try apply Sigma_algebra_Gen.
intros A HA; induction HA as [ | | A HA1 [HA2 | HA2] | A HA1 HA2]; try easy.
now left.
right; rewrite HA2; apply compl_empty.
left; rewrite HA2; apply compl_full.
case (classic ( n, A n = fullset)); intros H.
right; now apply union_seq_full.
left; apply union_seq_empty; intros n; destruct (HA2 n) as [HA2' | HA2']; try easy.
contradict H; now n.
Qed.

Definition discete_SA := @fullset (U Prop).

Lemma is_Sigma_algebra_discrete_SA : is_Sigma_algebra discete_SA.
Proof.
apply Ext_equiv; split; try easy.
apply Sigma_algebra_Gen.
Qed.

End More_Facts.

Require Import sigma_algebra.

Section equiv_SA.

Context {E : Type}.
Variable gen : (E Prop) Prop.

Lemma measurable_Sigma_algebra : measurable gen = Sigma_algebra gen.
Proof.
apply subset_ext; intro; split; intros H; induction H.
apply Sigma_algebra_Gen; easy.
apply Sigma_algebra_wEmpty.
apply Sigma_algebra_Compl_rev; easy.
apply Sigma_algebra_Union_seq; easy.
apply measurable_gen; easy.
apply measurable_empty.
apply measurable_compl_rev; easy.
apply measurable_union_countable; easy.
Qed.

End equiv_SA.

Section equiv_GP.

Context {U1 U2 : Type}.
Variable genU1 : (U1 Prop) Prop.
Variable genU2 : (U2 Prop) Prop.

Lemma Gen_Prod_Gen_Product : Gen_Prod genU1 genU2 = Gen_Product genU1 genU2.
Proof.
apply subset_ext; intro; split; intros [A1 [A2 [HA1 [HA2 HA]]]];
     A1, A2; (split; [easy | split; [easy |]]).
rewrite HA; easy.
apply subset_ext; easy.
Qed.

End equiv_GP.