Grace/Cumulus/Lattice/Complete.g17

Open in Workbench Download source

Imports

Bounded

Declarations

Source

1-- Complete lattices, arbitrary suprema and infima, and the powerset lattice2-- 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.Lattice.Complete8import Bounded910predicate IsCompleteLattice (A r : Set) :=11  IsPartialOrder(A, r) ∧ (∀ S, S ⊆ A → ∃ s, Supremum(A, r, S, s))1213def lowerBoundsOf (A r S : Set) : Set := { b ∈ A | LowerBound(A, r, S, b) }14def upperBoundsOf (A r S : Set) : Set := { b ∈ A | UpperBound(A, r, S, b) }1516theorem lowerBoundsOf.subset (A r S : Set)17  shows lowerBoundsOf(A, r, S) ⊆ A18proof19  intros b hb20  have member := lowerBoundsOf.membership.forward with hb21  exact member.left2223theorem upperBoundsOf.subset (A r S : Set)24  shows upperBoundsOf(A, r, S) ⊆ A25proof26  intros b hb27  have member := upperBoundsOf.membership.forward with hb28  exact member.left2930theorem IsCompleteLattice.order (A r : Set)31  requires h : IsCompleteLattice(A, r)32  shows IsPartialOrder(A, r)33proof34  simp [IsCompleteLattice]3536theorem IsCompleteLattice.exists_supremum (A r S : Set)37  requires h : IsCompleteLattice(A, r)38  requires hS : S ⊆ A39  shows ∃ s, Supremum(A, r, S, s)40proof41  rcases h with ⟨order, suprema⟩42  exact suprema with S, hS4344-- The infimum of S is the supremum of its lower bounds.4546theorem IsCompleteLattice.exists_infimum (A r S : Set)47  requires h : IsCompleteLattice(A, r)48  requires hS : S ⊆ A49  shows ∃ i, Infimum(A, r, S, i)50proof51  have lowerSubset := lowerBoundsOf.subset at A, r, S52  obtain ⟨s, hs⟩ := IsCompleteLattice.exists_supremum with h, lowerSubset53  have sA := Supremum.member with hs54  witness s55  constructor56  . refine ⟨sA, hS, ?_⟩57    intros x hx58    have xA := hS with x, hx59    have bound : UpperBound(A, r, lowerBoundsOf(A, r, S), x)60      refine ⟨xA, lowerSubset, ?_⟩61      intros b hb62      have member := lowerBoundsOf.membership.forward with hb63      exact LowerBound.below with member.right, hx64    exact Supremum.least with hs, xA, bound65  . intros b hb bound66    have member : b ∈ lowerBoundsOf(A, r, S) :=67      lowerBoundsOf.membership.backward with ⟨hb, bound⟩68    exact Supremum.above with hs, member6970-- Dually, a partial order with all infima has all suprema.7172theorem IsCompleteLattice.of_infima (A r : Set)73  requires order : IsPartialOrder(A, r)74  requires infima : ∀ S, S ⊆ A → ∃ i, Infimum(A, r, S, i)75  shows IsCompleteLattice(A, r)76proof77  constructor78  . exact order79  . intros S hS80    have upperSubset := upperBoundsOf.subset at A, r, S81    obtain ⟨i, hi⟩ := infima with upperBoundsOf(A, r, S), upperSubset82    have iA := Infimum.member with hi83    witness i84    constructor85    . refine ⟨iA, hS, ?_⟩86      intros x hx87      have xA := hS with x, hx88      have bound : LowerBound(A, r, upperBoundsOf(A, r, S), x)89        refine ⟨xA, upperSubset, ?_⟩90        intros b hb91        have member := upperBoundsOf.membership.forward with hb92        exact UpperBound.above with member.right, hx93      exact Infimum.greatest with hi, xA, bound94    . intros b hb bound95      have member : b ∈ upperBoundsOf(A, r, S) :=96        upperBoundsOf.membership.backward with ⟨hb, bound⟩97      exact Infimum.below with hi, member9899theorem IsCompleteLattice.lattice (A r : Set)100  requires h : IsCompleteLattice(A, r)101  shows IsLattice(A, r)102proof103  apply IsLattice.of_pairs with (IsCompleteLattice.order with h)104  . intros x hx y hy105    have bounded : {x, y} ⊆ A by simp106    exact IsCompleteLattice.exists_supremum with h, bounded107  . intros x hx y hy108    have bounded : {x, y} ⊆ A by simp109    exact IsCompleteLattice.exists_infimum with h, bounded110111theorem IsCompleteLattice.converse (A r : Set)112  requires h : IsCompleteLattice(A, r)113  shows IsCompleteLattice(A, converse(r, A, A))114proof115  have order := IsCompleteLattice.order with h116  apply IsCompleteLattice.of_infima with (IsPartialOrder.converse with order)117  intros S hS118  obtain ⟨s, hs⟩ := IsCompleteLattice.exists_supremum with h, hS119  refine ⟨s, Supremum.converse with hs⟩120121-- The supremum and infimum of a subset122123defunique supremum (A r S : Set) (s ∈ A) := Supremum(A, r, S, s)124requires complete : IsCompleteLattice(A, r)125requires hS : S ⊆ A126proof127  obtain ⟨s, hs⟩ := IsCompleteLattice.exists_supremum with complete, hS128  witness s129  refine ⟨Supremum.member with hs, hs⟩130uniqueness131  intros s sA first t tA second132  exact Supremum.unique with (IsCompleteLattice.order with complete), first,133      second134135defunique infimum (A r S : Set) (i ∈ A) := Infimum(A, r, S, i)136requires complete : IsCompleteLattice(A, r)137requires hS : S ⊆ A138proof139  obtain ⟨i, hi⟩ := IsCompleteLattice.exists_infimum with complete, hS140  witness i141  refine ⟨Infimum.member with hi, hi⟩142uniqueness143  intros i iA first j jA second144  exact Infimum.unique with (IsCompleteLattice.order with complete), first,145    second146147theorem supremum.member (A r S : Set)148  requires complete : IsCompleteLattice(A, r)149  requires hS : S ⊆ A150  shows supremum(A, r, S) ∈ A151proof152  have selected := supremum.selected with complete, hS153  exact selected.left154155theorem supremum.supremum (A r S : Set)156  requires complete : IsCompleteLattice(A, r)157  requires hS : S ⊆ A158  shows Supremum(A, r, S, supremum(A, r, S))159proof160  have selected := supremum.selected with complete, hS161  exact selected.right162163theorem supremum.upper (A r S : Set)164  requires complete : IsCompleteLattice(A, r)165  requires hS : S ⊆ A166  shows UpperBound(A, r, S, supremum(A, r, S))167proof168  exact Supremum.upper with (supremum.supremum with complete, hS)169170theorem supremum.above (A r S x : Set)171  requires complete : IsCompleteLattice(A, r)172  requires hS : S ⊆ A173  requires hx : x ∈ S174  shows relates(r, x, supremum(A, r, S))175proof176  exact Supremum.above with (supremum.supremum with complete, hS), hx177178theorem supremum.least (A r S b : Set)179  requires complete : IsCompleteLattice(A, r)180  requires hS : S ⊆ A181  requires hb : b ∈ A182  requires bound : UpperBound(A, r, S, b)183  shows relates(r, supremum(A, r, S), b)184proof185  exact Supremum.least with (supremum.supremum with complete, hS), hb, bound186187theorem supremum.of_supremum (A r S s : Set)188  requires complete : IsCompleteLattice(A, r)189  requires hS : S ⊆ A190  requires h : Supremum(A, r, S, s)191  shows s = supremum(A, r, S)192proof193  have order := IsCompleteLattice.order with complete194  exact Supremum.unique with order, h, (supremum.supremum with complete, hS)195196theorem supremum.le_iff (A r S b : Set)197  requires complete : IsCompleteLattice(A, r)198  requires hS : S ⊆ A199  requires hb : b ∈ A200  shows relates(r, supremum(A, r, S), b) ↔ ∀ x ∈ S, relates(r, x, b)201proof202  have order := IsCompleteLattice.order with complete203  have transitive := IsPartialOrder.transitive with order204  have supA := supremum.member with complete, hS205  constructor206  . intros below x hx207    have above := supremum.above with complete, hS, hx208    exact transitive with x, (hS with x, hx), supremum(A, r, S), supA, b, hb,209        above, below210  . intro bounds211    exact supremum.least with complete, hS, hb, ⟨hb, hS, bounds⟩212213theorem infimum.member (A r S : Set)214  requires complete : IsCompleteLattice(A, r)215  requires hS : S ⊆ A216  shows infimum(A, r, S) ∈ A217proof218  have selected := infimum.selected with complete, hS219  exact selected.left220221theorem infimum.infimum (A r S : Set)222  requires complete : IsCompleteLattice(A, r)223  requires hS : S ⊆ A224  shows Infimum(A, r, S, infimum(A, r, S))225proof226  have selected := infimum.selected with complete, hS227  exact selected.right228229theorem infimum.lower (A r S : Set)230  requires complete : IsCompleteLattice(A, r)231  requires hS : S ⊆ A232  shows LowerBound(A, r, S, infimum(A, r, S))233proof234  exact Infimum.lower with (infimum.infimum with complete, hS)235236theorem infimum.below (A r S x : Set)237  requires complete : IsCompleteLattice(A, r)238  requires hS : S ⊆ A239  requires hx : x ∈ S240  shows relates(r, infimum(A, r, S), x)241proof242  exact Infimum.below with (infimum.infimum with complete, hS), hx243244theorem infimum.greatest (A r S b : Set)245  requires complete : IsCompleteLattice(A, r)246  requires hS : S ⊆ A247  requires hb : b ∈ A248  requires bound : LowerBound(A, r, S, b)249  shows relates(r, b, infimum(A, r, S))250proof251  exact Infimum.greatest with (infimum.infimum with complete, hS), hb, bound252253theorem infimum.of_infimum (A r S i : Set)254  requires complete : IsCompleteLattice(A, r)255  requires hS : S ⊆ A256  requires h : Infimum(A, r, S, i)257  shows i = infimum(A, r, S)258proof259  have order := IsCompleteLattice.order with complete260  exact Infimum.unique with order, h, (infimum.infimum with complete, hS)261262theorem infimum.ge_iff (A r S b : Set)263  requires complete : IsCompleteLattice(A, r)264  requires hS : S ⊆ A265  requires hb : b ∈ A266  shows relates(r, b, infimum(A, r, S)) ↔ ∀ x ∈ S, relates(r, b, x)267proof268  have order := IsCompleteLattice.order with complete269  have transitive := IsPartialOrder.transitive with order270  have infA := infimum.member with complete, hS271  constructor272  . intros above x hx273    have below := infimum.below with complete, hS, hx274    exact transitive with b, hb, infimum(A, r, S), infA, x, (hS with x, hx),275        above, below276  . intro bounds277    exact infimum.greatest with complete, hS, hb, ⟨hb, hS, bounds⟩278279-- Monotonicity, pairs, singletons, the empty set, and the whole points280281theorem supremum.monotone (A r S T : Set)282  requires complete : IsCompleteLattice(A, r)283  requires hST : S ⊆ T284  requires hT : T ⊆ A285  shows relates(r, supremum(A, r, S), supremum(A, r, T))286proof287  have hS := Subset.transitive with hST, hT288  have supS := supremum.supremum with complete, hS289  have supT := supremum.supremum with complete, hT290  exact Supremum.monotone with hST, supS, supT291292theorem infimum.antitone (A r S T : Set)293  requires complete : IsCompleteLattice(A, r)294  requires hST : S ⊆ T295  requires hT : T ⊆ A296  shows relates(r, infimum(A, r, T), infimum(A, r, S))297proof298  have hS := Subset.transitive with hST, hT299  have infS := infimum.infimum with complete, hS300  have infT := infimum.infimum with complete, hT301  exact Infimum.antitone with hST, infS, infT302303theorem supremum.pair (A r x y : Set)304  requires complete : IsCompleteLattice(A, r)305  requires hx : x ∈ A306  requires hy : y ∈ A307  shows supremum(A, r, {x, y}) = join(A, r, x, y)308proof309  have lattice := IsCompleteLattice.lattice with complete310  have bounded : {x, y} ⊆ A by simp311  have supremum := supremum.supremum with complete, bounded312  exact join.of_supremum with lattice, hx, hy, supremum313314theorem infimum.pair (A r x y : Set)315  requires complete : IsCompleteLattice(A, r)316  requires hx : x ∈ A317  requires hy : y ∈ A318  shows infimum(A, r, {x, y}) = meet(A, r, x, y)319proof320  have lattice := IsCompleteLattice.lattice with complete321  have bounded : {x, y} ⊆ A by simp322  have infimum := infimum.infimum with complete, bounded323  exact meet.of_infimum with lattice, hx, hy, infimum324325theorem supremum.singleton (A r x : Set)326  requires complete : IsCompleteLattice(A, r)327  requires hx : x ∈ A328  shows supremum(A, r, {x}) = x329proof330  have order := IsCompleteLattice.order with complete331  have bounded : {x} ⊆ A by simp332  symm333  exact supremum.of_supremum with complete, bounded,334      (Supremum.singleton with order, hx)335336theorem infimum.singleton (A r x : Set)337  requires complete : IsCompleteLattice(A, r)338  requires hx : x ∈ A339  shows infimum(A, r, {x}) = x340proof341  have order := IsCompleteLattice.order with complete342  have bounded : {x} ⊆ A by simp343  symm344  exact infimum.of_infimum with complete, bounded,345      (Infimum.singleton with order, hx)346347theorem supremum.empty (A r : Set)348  requires complete : IsCompleteLattice(A, r)349  shows Least(A, r, A, supremum(A, r, ∅))350proof351  have supremum := supremum.supremum with complete, (empty.subset at A)352  exact Supremum.empty_iff.forward with supremum353354theorem infimum.empty (A r : Set)355  requires complete : IsCompleteLattice(A, r)356  shows Greatest(A, r, A, infimum(A, r, ∅))357proof358  have infimum := infimum.infimum with complete, (empty.subset at A)359  exact Infimum.empty_iff.forward with infimum360361theorem supremum.whole (A r : Set)362  requires complete : IsCompleteLattice(A, r)363  shows Greatest(A, r, A, supremum(A, r, A))364proof365  have supremum := supremum.supremum with complete, (Subset.reflexive at A)366  exact Supremum.whole_iff.forward with supremum367368theorem infimum.whole (A r : Set)369  requires complete : IsCompleteLattice(A, r)370  shows Least(A, r, A, infimum(A, r, A))371proof372  have infimum := infimum.infimum with complete, (Subset.reflexive at A)373  exact Infimum.whole_iff.forward with infimum374375theorem IsCompleteLattice.bounded (A r : Set)376  requires complete : IsCompleteLattice(A, r)377  shows IsBoundedLattice(A, r, supremum(A, r, ∅), supremum(A, r, A))378proof379  have lattice := IsCompleteLattice.lattice with complete380  exact IsBoundedLattice.of_bounds with lattice, (supremum.empty with complete),381      (supremum.whole with complete)382383theorem IsCompleteLattice.nonempty (A r : Set)384  requires complete : IsCompleteLattice(A, r)385  shows Nonempty(A)386proof387  exact IsBoundedLattice.nonempty with (IsCompleteLattice.bounded with complete)388389theorem supremum.union2 (A r S T : Set)390  requires complete : IsCompleteLattice(A, r)391  requires hS : S ⊆ A392  requires hT : T ⊆ A393  shows supremum(A, r, S ∪ T) = join(A, r, supremum(A, r, S), supremum(A, r, T))394proof395  have lattice := IsCompleteLattice.lattice with complete396  have transitive := IsLattice.transitive with lattice397  have hST := union2.subset with hS, hT398  have supS := supremum.member with complete, hS399  have supT := supremum.member with complete, hT400  have joinA := join.member with lattice, supS, supT401  have sJ := join.upper_left with lattice, supS, supT402  have tJ := join.upper_right with lattice, supS, supT403  have result : Supremum(A, r, S ∪ T, join(A, r, supremum(A, r, S),404      supremum(A, r, T)))405    constructor406    . refine ⟨joinA, hST, ?_⟩407      intros x hx408      have cases := union2.membership.forward with hx409      cases cases with xS | xT410      . have above := supremum.above with complete, hS, xS411        exact transitive with x, (hS with x, xS), supremum(A, r, S), supS,412            join(A, r, supremum(A, r, S), supremum(A, r, T)), joinA, above, sJ413      . have above := supremum.above with complete, hT, xT414        exact transitive with x, (hT with x, xT), supremum(A, r, T), supT,415            join(A, r, supremum(A, r, S), supremum(A, r, T)), joinA, above, tJ416    . intros b hb bound417      have boundS := UpperBound.antitone with (union2.subset_left at S, T),418          bound419      have boundT := UpperBound.antitone with (union2.subset_right at S, T),420          bound421      have sb := supremum.least with complete, hS, hb, boundS422      have tb := supremum.least with complete, hT, hb, boundT423      exact join.least with lattice, supS, supT, hb, sb, tb424  symm425  exact supremum.of_supremum with complete, hST, result426427theorem infimum.union2 (A r S T : Set)428  requires complete : IsCompleteLattice(A, r)429  requires hS : S ⊆ A430  requires hT : T ⊆ A431  shows infimum(A, r, S ∪ T) = meet(A, r, infimum(A, r, S), infimum(A, r, T))432proof433  have lattice := IsCompleteLattice.lattice with complete434  have transitive := IsLattice.transitive with lattice435  have hST := union2.subset with hS, hT436  have infS := infimum.member with complete, hS437  have infT := infimum.member with complete, hT438  have meetA := meet.member with lattice, infS, infT439  have mS := meet.lower_left with lattice, infS, infT440  have mT := meet.lower_right with lattice, infS, infT441  have result : Infimum(A, r, S ∪ T, meet(A, r, infimum(A, r, S), infimum(A,442      r, T)))443    constructor444    . refine ⟨meetA, hST, ?_⟩445      intros x hx446      have cases := union2.membership.forward with hx447      cases cases with xS | xT448      . have below := infimum.below with complete, hS, xS449        exact transitive with meet(A, r, infimum(A, r, S), infimum(A, r, T)),450            meetA, infimum(A, r, S), infS, x, (hS with x, xS), mS, below451      . have below := infimum.below with complete, hT, xT452        exact transitive with meet(A, r, infimum(A, r, S), infimum(A, r, T)),453            meetA, infimum(A, r, T), infT, x, (hT with x, xT), mT, below454    . intros b hb bound455      have boundS := LowerBound.antitone with (union2.subset_left at S, T),456          bound457      have boundT := LowerBound.antitone with (union2.subset_right at S, T),458          bound459      have bs := infimum.greatest with complete, hS, hb, boundS460      have bt := infimum.greatest with complete, hT, hb, boundT461      exact meet.greatest with lattice, infS, infT, hb, bs, bt462  symm463  exact infimum.of_infimum with complete, hST, result464465-- The powerset of a set, ordered by inclusion, is a complete lattice whose466-- suprema are unions and whose infima are intersections relative to X.467468def powersetOrder (X : Set) : Set := inclusionOrder(𝒫(X))469470theorem powersetOrder.relates (X B C : Set)471  requires hB : B ∈ 𝒫(X)472  requires hC : C ∈ 𝒫(X)473  shows relates(powersetOrder(X), B, C) ↔ B ⊆ C474proof475  have characterization := inclusionOrder.relates with hB, hC476  simpa [powersetOrder] using characterization477478theorem powersetOrder.partial (X : Set)479  shows IsPartialOrder(𝒫(X), powersetOrder(X))480proof481  have partial := inclusionOrder.partial at 𝒫(X)482  simpa [powersetOrder] using partial483484def relativeIntersection (X S : Set) : Set := { x ∈ X | ∀ B ∈ S, x ∈ B }485486theorem relativeIntersection.subset (X S : Set)487  shows relativeIntersection(X, S) ⊆ X488proof489  intros x hx490  have member := relativeIntersection.membership.forward with hx491  exact member.left492493theorem powersetOrder.supremum (X S : Set)494  requires hS : S ⊆ 𝒫(X)495  shows Supremum(𝒫(X), powersetOrder(X), S, ⋃(S))496proof497  have unionIn : ⋃(S) ∈ 𝒫(X)498    apply powerset.membership_iff.backward499    apply union.subset500    intros B hB501    exact powerset.membership_iff.forward with (hS with B, hB)502  constructor503  . refine ⟨unionIn, hS, ?_⟩504    intros B hB505    have BIn := hS with B, hB506    apply powersetOrder.relates.backward with BIn, unionIn507    exact union.subset_of_member with hB508  . intros b hb bound509    apply powersetOrder.relates.backward with unionIn, hb510    apply union.subset511    intros B hB512    have related := UpperBound.above with bound, hB513    exact powersetOrder.relates.forward with (hS with B, hB), hb, related514515theorem powersetOrder.infimum (X S : Set)516  requires hS : S ⊆ 𝒫(X)517  shows Infimum(𝒫(X), powersetOrder(X), S, relativeIntersection(X, S))518proof519  have interIn : relativeIntersection(X, S) ∈ 𝒫(X) :=520    powerset.membership_iff.backward with (relativeIntersection.subset at X, S)521  constructor522  . refine ⟨interIn, hS, ?_⟩523    intros B hB524    apply powersetOrder.relates.backward with interIn, (hS with B, hB)525    intros x hx526    have member := relativeIntersection.membership.forward with hx527    exact member.right with B, hB528  . intros b hb bound529    apply powersetOrder.relates.backward with hb, interIn530    intros x hx531    have bX := powerset.membership_iff.forward with hb532    apply relativeIntersection.membership.backward533    constructor534    . exact bX with x, hx535    . intros B hB536      have related := LowerBound.below with bound, hB537      have subset := powersetOrder.relates.forward with hb, (hS with B, hB),538          related539      exact subset with x, hx540541theorem IsCompleteLattice.powerset (X : Set)542  shows IsCompleteLattice(𝒫(X), powersetOrder(X))543proof544  constructor545  . exact powersetOrder.partial at X546  . intros S hS547    refine ⟨⋃(S), powersetOrder.supremum with hS⟩548549theorem powersetOrder.lattice (X : Set)550  shows IsLattice(𝒫(X), powersetOrder(X))551proof552  exact IsCompleteLattice.lattice with (IsCompleteLattice.powerset at X)553554theorem powersetOrder.supremum_value (X S : Set)555  requires hS : S ⊆ 𝒫(X)556  shows supremum(𝒫(X), powersetOrder(X), S) = ⋃(S)557proof558  have complete := IsCompleteLattice.powerset at X559  symm560  exact supremum.of_supremum with complete, hS, (powersetOrder.supremum with hS)561562theorem powersetOrder.infimum_value (X S : Set)563  requires hS : S ⊆ 𝒫(X)564  shows infimum(𝒫(X), powersetOrder(X), S) = relativeIntersection(X, S)565proof566  have complete := IsCompleteLattice.powerset at X567  symm568  exact infimum.of_infimum with complete, hS, (powersetOrder.infimum with hS)569570theorem powersetOrder.join (X B C : Set)571  requires hB : B ∈ 𝒫(X)572  requires hC : C ∈ 𝒫(X)573  shows join(𝒫(X), powersetOrder(X), B, C) = B ∪ C574proof575  have lattice := powersetOrder.lattice at X576  have BX := powerset.membership_iff.forward with hB577  have CX := powerset.membership_iff.forward with hC578  have unionIn : B ∪ C ∈ 𝒫(X) :=579    powerset.membership_iff.backward with (union2.subset with BX, CX)580  have leftIn := powersetOrder.relates.backward with hB, unionIn,581      (union2.subset_left at B, C)582  have rightIn := powersetOrder.relates.backward with hC, unionIn,583      (union2.subset_right at B, C)584  have supremum : Supremum(𝒫(X), powersetOrder(X), {B, C}, B ∪ C)585    apply Supremum.of_pair with hB, hC, unionIn, leftIn, rightIn586    intros D hD BD CD587    have BDsubset := powersetOrder.relates.forward with hB, hD, BD588    have CDsubset := powersetOrder.relates.forward with hC, hD, CD589    apply powersetOrder.relates.backward with unionIn, hD590    exact union2.subset with BDsubset, CDsubset591  symm592  exact join.of_supremum with lattice, hB, hC, supremum593594theorem powersetOrder.meet (X B C : Set)595  requires hB : B ∈ 𝒫(X)596  requires hC : C ∈ 𝒫(X)597  shows meet(𝒫(X), powersetOrder(X), B, C) = B ∩ C598proof599  have lattice := powersetOrder.lattice at X600  have BX := powerset.membership_iff.forward with hB601  have interIn : B ∩ C ∈ 𝒫(X) :=602    powerset.membership_iff.backward with (Subset.transitive with (intersection.subset_left at B, C), BX)603  have leftIn := powersetOrder.relates.backward with interIn, hB,604      (intersection.subset_left at B, C)605  have rightIn := powersetOrder.relates.backward with interIn, hC,606      (intersection.subset_right at B, C)607  have infimum : Infimum(𝒫(X), powersetOrder(X), {B, C}, B ∩ C)608    apply Infimum.of_pair with hB, hC, interIn, leftIn, rightIn609    intros D hD DB DC610    have DBsubset := powersetOrder.relates.forward with hD, hB, DB611    have DCsubset := powersetOrder.relates.forward with hD, hC, DC612    apply powersetOrder.relates.backward with hD, interIn613    exact intersection.greatest with DBsubset, DCsubset614  symm615  exact meet.of_infimum with lattice, hB, hC, infimum616617theorem powersetOrder.bounded (X : Set)618  shows IsBoundedLattice(𝒫(X), powersetOrder(X), ∅, X)619proof620  have lattice := powersetOrder.lattice at X621  have emptyIn := powerset.empty_member at X622  have selfIn := powerset.self at X623  apply IsBoundedLattice.of_bounds with lattice624  . constructor625    . exact emptyIn626    . refine ⟨emptyIn, Subset.reflexive at 𝒫(X), ?_⟩627      intros B hB628      exact powersetOrder.relates.backward with emptyIn, hB, (empty.subset at B)629  . constructor630    . exact selfIn631    . refine ⟨selfIn, Subset.reflexive at 𝒫(X), ?_⟩632      intros B hB633      exact powersetOrder.relates.backward with hB, selfIn,634          (powerset.membership_iff.forward with hB)635