Grace/Cumulus/Set/MaximalPrinciple.g17

Open in Workbench Download source

Imports

Zorn

Declarations

Source

1-- Maximal extensions in families closed under nonempty chain unions.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Set.MaximalPrinciple8import Zorn910def extensions (F I : Set) : Set := {J ∈ F | I ⊆ J}1112theorem inclusionChain.nested (F S : Set)13  requires chain : Chain(F, inclusionOrder(F), S)14  shows ∀ C ∈ S, ∀ D ∈ S, C ⊆ D ∨ D ⊆ C15proof16  rcases chain with ⟨bounded, comparable⟩17  intros C hC D hD18  have memberC := bounded with C, hC19  have memberD := bounded with D, hD20  have directions := comparable with C, hC, D, hD21  have forward := inclusionOrder.relates at F, C, D with *22  have backward := inclusionOrder.relates at F, D, C with *23  cases directions with cd | dc24  . left25    exact forward.forward with cd26  . right27    exact backward.forward with dc2829-- Only nonempty unions are required; I supplies the empty-chain bound.30theorem maximal_extension (F I : Set)31  requires seed : I ∈ F32  requires closed : ∀ S, Nonempty(S) → S ⊆ F →33    (∀ C ∈ S, ∀ D ∈ S, C ⊆ D ∨ D ⊆ C) → ⋃(S) ∈ F34  shows ∃ M ∈ F, I ⊆ M ∧ (∀ J ∈ F, M ⊆ J → J = M)35proof36  have self := Subset.reflexive at I37  have seedMember : I ∈ extensions(F, I) := extensions.membership.backward with ⟨seed, self⟩38  have condition : ZornCondition(extensions(F, I), inclusionOrder(extensions(F, I)))39    constructor40    . exact inclusionOrder.partial at extensions(F, I)41    . intros S chain42      have subset := Chain.subset with chain43      have nested := inclusionChain.nested with chain44      have alternatives : Nonempty(S) ∨ ¬Nonempty(S) by tauto45      cases alternatives with inhabited | absent46      . have subsetF : S ⊆ F47          intros J hJ48          have member := subset with J, hJ49          obtain ⟨inFamily, extendsJ⟩ := extensions.membership.forward with member50          exact inFamily51        have unionF := closed with S, inhabited, subsetF, nested52        have extends : I ⊆ ⋃(S)53          obtain ⟨seedChain, hJ⟩ := inhabited54          have member := subset with seedChain, hJ55          obtain ⟨inFamily, contains⟩ := extensions.membership.forward with member56          intros x hx57          have inJ := contains with x, hx58          exact set.union.backward with ⟨seedChain, hJ, inJ⟩59        have unionMember : ⋃(S) ∈ extensions(F, I) := extensions.membership.backward with ⟨unionF, extends⟩60        witness ⋃(S)61        refine ⟨unionMember, subset, ?_⟩62        intros J hJ63        have member := subset with J, hJ64        apply inclusionOrder.relates.backward with member, unionMember65        intros x hx66        exact set.union.backward with ⟨J, hJ, hx⟩67      . witness I68        refine ⟨seedMember, subset, ?_⟩69        intros J hJ70        exfalso71        exact absent with ⟨J, hJ⟩72  obtain ⟨M, memberM, greatest⟩ := Zorn.theorem with condition73  obtain ⟨inF, extends⟩ := extensions.membership.forward with memberM74  refine ⟨M, inF, extends, ?_⟩75  intros J hJ contains76  have extendsJ := Subset.transitive with extends, contains77  have memberJ : J ∈ extensions(F, I) := extensions.membership.backward with ⟨hJ, extendsJ⟩78  have edge := inclusionOrder.relates.backward with memberM, memberJ, contains79  exact greatest with J, memberJ, edge8081theorem Chain.extends_maximal (A r I : Set)82  requires initial : Chain(A, r, I)83  shows ∃ M, Chain(A, r, M) ∧ I ⊆ M ∧84    (∀ J, Chain(A, r, J) → M ⊆ J → J = M)85proof86  have seed := chains.contains with initial87  have closed : ∀ S, Nonempty(S) → S ⊆ chains(A, r) →88    (∀ C ∈ S, ∀ D ∈ S, C ⊆ D ∨ D ⊆ C) → ⋃(S) ∈ chains(A, r)89    intros S inhabited subset nested90    have family : ChainOfChains(A, r, S)91      constructor92      . intros C hC93        have member := subset with C, hC94        obtain ⟨boundedC, chainC⟩ := chains.membership.forward with member95        exact chainC96      . exact nested97    have unionChain := Chain.union with family98    exact chains.contains with unionChain99  obtain ⟨M, member, extends, maximal⟩ := maximal_extension with seed, closed100  obtain ⟨boundedM, chainM⟩ := chains.membership.forward with member101  witness M102  constructor103  . exact chainM104  . constructor105    . exact extends106    . intros J chainJ contains107      have memberJ := chains.contains with chainJ108      exact maximal with J, memberJ, contains109110theorem Zorn.above (A r a : Set)111  requires condition : ZornCondition(A, r)112  requires start : a ∈ A113  shows ∃ m, Maximal(A, r, m) ∧ relates(r, a, m)114proof115  have order := ZornCondition.order with condition116  have singletonChain := Chain.singleton with order, start117  obtain ⟨C, chain, extends, maximalChain⟩ := Chain.extends_maximal with singletonChain118  rcases condition with ⟨partial, bounds⟩119  obtain ⟨m, bound⟩ := bounds with C, chain120  have extended := Chain.adjoin_upper with order, chain, bound121  have subset := union2.subset_left at C, {m}122  have equal := maximalChain with C ∪ {m}, extended, subset123  have mIn : m ∈ C124    have self := singleton.self at m125    have member := union2.right at m, C, {m} with self126    rwa equal at member127  rcases bound with ⟨mInA, subsetC, upper⟩128  have aIn : a ∈ C by exact extends with a, singleton.self at a129  have above := upper with a, aIn130  have maximal : Maximal(A, r, m)131    constructor132    . exact mInA133    . intros x hx mx134      have transitive := IsPartialOrder.transitive with order135      have boundX : UpperBound(A, r, C, x)136        constructor137        . exact hx138        . constructor139          . exact subsetC140          . intros y hy141            have ym := upper with y, hy142            have yInA : y ∈ A by exact subsetC with y, hy143            exact transitive with y, yInA, m, mInA, x, hx, ym, mx144      have chainX := Chain.adjoin_upper with order, chain, boundX145      have subsetX := union2.subset_left at C, {x}146      have equalX := maximalChain with C ∪ {x}, chainX, subsetX147      have xIn : x ∈ C148        have self := singleton.self at x149        have member := union2.right at x, C, {x} with self150        rwa equalX at member151      have xm := upper with x, xIn152      have antisymmetric := IsPartialOrder.antisymmetric with order153      exact antisymmetric with x, hx, m, mInA, xm, mx154  refine ⟨m, maximal, above⟩155