From 83d886ad288005ff86073d791619dc34bdb3e5f9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 17 Jul 2023 14:46:07 +0900 Subject: [PATCH 1/2] Zorn lemma for inclusion Co-authored-by: Takafumi Saikawa --- CHANGELOG_UNRELEASED.md | 3 +++ classical/classical_sets.v | 33 ++++++++++++++++++++++++++++----- 2 files changed, 31 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 949844bd5d..f272f30696 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -54,6 +54,9 @@ - in `classical_sets.v`: + lemmas `properW`, `properxx` +- in `classical_sets.v`: + + lemma `Zorn_bigcup` + ### Changed - moved from `lebesgue_measure.v` to `real_interval.v`: diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 1655043cc7..cddaa6d7bd 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2677,12 +2677,12 @@ Lemma Zorn T (R : T -> T -> Prop) : exists t, forall s, R t s -> s = t. Proof. move=> Rrefl Rtrans Rantisym Rtot_max. -set totR := ({A : set T | total_on A R}). +pose totR := {A : set T | total_on A R}. set R' := fun A B : totR => sval A `<=` sval B. have R'refl A : R' A A by []. have R'trans A B C : R' A B -> R' B C -> R' A C by apply: subset_trans. have R'antisym A B : R' A B -> R' B A -> A = B. - rewrite /R'; case: A; case: B => /= B totB A totA sAB sBA. + rewrite /R'; move: A B => [/= A totA] [/= B totB] sAB sBA. by apply: eq_exist; rewrite predeqE=> ?; split=> [/sAB|/sBA]. have R'tot_lub A : total_on A R' -> exists t, (forall s, A s -> R' s t) /\ forall r, (forall s, A s -> R' s r) -> R' t r. @@ -2693,7 +2693,7 @@ have R'tot_lub A : total_on A R' -> exists t, (forall s, A s -> R' s t) /\ by have /(_ _ _ Cs Ct) := svalP C. by have /(_ _ _ Bs Bt) := svalP B. exists (exist _ (\bigcup_(B in A) sval B) AUtot); split. - by move=> B ???; exists B. + by move=> B ? ? ?; exists B. by move=> B Bub ? /= [? /Bub]; apply. apply: contrapT => nomax. have {}nomax t : exists s, R t s /\ s <> t. @@ -2708,9 +2708,9 @@ have Astot : total_on (sval A `|` [set s]) R. by move=> [/tub Rvt|->]; right=> //; apply: Rtrans Rts. move=> [Av|->]; [apply: (svalP A)|left] => //. by apply: Rtrans Rts; apply: tub. -exists (exist _ (sval A `|` [set s]) Astot); split; first by move=> ??; left. +exists (exist _ (sval A `|` [set s]) Astot); split; first by move=> ? ?; left. split=> [AeAs|[B Btot] sAB sBAs]. - have [/tub Rst|] := (pselect (sval A s)); first exact/snet/Rantisym. + have [/tub Rst|] := pselect (sval A s); first exact/snet/Rantisym. by rewrite AeAs /=; apply; right. have [Bs|nBs] := pselect (B s). by right; apply: eq_exist; rewrite predeqE => r; split=> [/sBAs|[/sAB|->]]. @@ -2719,6 +2719,29 @@ apply: eq_exist; rewrite predeqE => r; split=> [Br|/sAB] //. by have /sBAs [|ser] // := Br; rewrite ser in Br. Qed. +Section Zorn_subset. +Variables (T : Type) (P : set T -> Prop). +Let sigP := {x | P x}. +Let R (sA sB : sigP) := sval sA `<=` sval sB. + +Lemma Zorn_bigcup : + (forall F, total_on F R -> P (\bigcup_(x in F) sval x)) -> + exists A, P A /\ forall B, A `<` B -> ~ P B. +Proof. +move=> totR. +have {}totR F : total_on F R -> exists sB, forall sA, F sA -> R sA sB. + by move=> FR; exists (exist _ _ (totR _ FR)) => sA FsA; exact: bigcup_sup. +have [| | |sA sAmax] := Zorn _ _ _ totR. +- by move=> ?; exact: subset_refl. +- by move=> ? ? ?; exact: subset_trans. +- by move=> [A PA] [B PB]; rewrite /R /= => AB BA; exact/eq_exist/seteqP. +- exists (sval sA); case: sA => A PA in sAmax *; split => //= B AB PB. + have [BA] := sAmax (exist _ B PB) (properW AB). + by move: AB; rewrite BA; exact: properxx. +Qed. + +End Zorn_subset. + Definition premaximal T (R : T -> T -> Prop) (t : T) := forall s, R t s -> R s t. From d6b34ae937dae635fe8fdcb9f88f0f8f13099680 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 19 Jul 2023 22:33:24 +0900 Subject: [PATCH 2/2] Zorn inclusion by Cyril Co-authored-by: Cyril Cohen --- classical/classical_sets.v | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index cddaa6d7bd..4b6a0c008f 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2720,23 +2720,27 @@ by have /sBAs [|ser] // := Br; rewrite ser in Br. Qed. Section Zorn_subset. -Variables (T : Type) (P : set T -> Prop). -Let sigP := {x | P x}. -Let R (sA sB : sigP) := sval sA `<=` sval sB. +Variables (T : Type) (P : set (set T)). Lemma Zorn_bigcup : - (forall F, total_on F R -> P (\bigcup_(x in F) sval x)) -> + (forall F : set (set T), F `<=` P -> total_on F subset -> + P (\bigcup_(X in F) X)) -> exists A, P A /\ forall B, A `<` B -> ~ P B. Proof. -move=> totR. -have {}totR F : total_on F R -> exists sB, forall sA, F sA -> R sA sB. - by move=> FR; exists (exist _ _ (totR _ FR)) => sA FsA; exact: bigcup_sup. +move=> totP; pose R (sA sB : P) := sval sA `<=` sval sB. +have {}totR F (FR : total_on F R) : exists sB, forall sA, F sA -> R sA sB. + have FP : [set val x | x in F] `<=` P. + by move=> _ [X FX <-]; apply: set_mem; apply: valP. + have totF : total_on [set val x | x in F] subset. + by move=> _ _ [X FX <-] [Y FY <-]; apply: FR. + exists (SigSub (mem_set (totP _ FP totF))) => A FA; rewrite /R/=. + exact: (bigcup_sup (imageP val _)). have [| | |sA sAmax] := Zorn _ _ _ totR. - by move=> ?; exact: subset_refl. - by move=> ? ? ?; exact: subset_trans. - by move=> [A PA] [B PB]; rewrite /R /= => AB BA; exact/eq_exist/seteqP. -- exists (sval sA); case: sA => A PA in sAmax *; split => //= B AB PB. - have [BA] := sAmax (exist _ B PB) (properW AB). +- exists (val sA); case: sA => A PA /= in sAmax *; split; first exact: set_mem. + move=> B AB PB; have [BA] := sAmax (SigSub (mem_set PB)) (properW AB). by move: AB; rewrite BA; exact: properxx. Qed.