-- Complete lattices, arbitrary suprema and infima, and the powerset lattice
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Lattice.Complete
import Bounded

predicate IsCompleteLattice (A r : Set) :=
  IsPartialOrder(A, r) ∧ (∀ S, S ⊆ A → ∃ s, Supremum(A, r, S, s))

def lowerBoundsOf (A r S : Set) : Set := { b ∈ A | LowerBound(A, r, S, b) }
def upperBoundsOf (A r S : Set) : Set := { b ∈ A | UpperBound(A, r, S, b) }

theorem lowerBoundsOf.subset (A r S : Set)
  shows lowerBoundsOf(A, r, S) ⊆ A
proof
  intros b hb
  have member := lowerBoundsOf.membership.forward with hb
  exact member.left

theorem upperBoundsOf.subset (A r S : Set)
  shows upperBoundsOf(A, r, S) ⊆ A
proof
  intros b hb
  have member := upperBoundsOf.membership.forward with hb
  exact member.left

theorem IsCompleteLattice.order (A r : Set)
  requires h : IsCompleteLattice(A, r)
  shows IsPartialOrder(A, r)
proof
  simp [IsCompleteLattice]

theorem IsCompleteLattice.exists_supremum (A r S : Set)
  requires h : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  shows ∃ s, Supremum(A, r, S, s)
proof
  rcases h with ⟨order, suprema⟩
  exact suprema with S, hS

-- The infimum of S is the supremum of its lower bounds.

theorem IsCompleteLattice.exists_infimum (A r S : Set)
  requires h : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  shows ∃ i, Infimum(A, r, S, i)
proof
  have lowerSubset := lowerBoundsOf.subset at A, r, S
  obtain ⟨s, hs⟩ := IsCompleteLattice.exists_supremum with h, lowerSubset
  have sA := Supremum.member with hs
  witness s
  constructor
  . refine ⟨sA, hS, ?_⟩
    intros x hx
    have xA := hS with x, hx
    have bound : UpperBound(A, r, lowerBoundsOf(A, r, S), x)
      refine ⟨xA, lowerSubset, ?_⟩
      intros b hb
      have member := lowerBoundsOf.membership.forward with hb
      exact LowerBound.below with member.right, hx
    exact Supremum.least with hs, xA, bound
  . intros b hb bound
    have member : b ∈ lowerBoundsOf(A, r, S) :=
      lowerBoundsOf.membership.backward with ⟨hb, bound⟩
    exact Supremum.above with hs, member

-- Dually, a partial order with all infima has all suprema.

theorem IsCompleteLattice.of_infima (A r : Set)
  requires order : IsPartialOrder(A, r)
  requires infima : ∀ S, S ⊆ A → ∃ i, Infimum(A, r, S, i)
  shows IsCompleteLattice(A, r)
proof
  constructor
  . exact order
  . intros S hS
    have upperSubset := upperBoundsOf.subset at A, r, S
    obtain ⟨i, hi⟩ := infima with upperBoundsOf(A, r, S), upperSubset
    have iA := Infimum.member with hi
    witness i
    constructor
    . refine ⟨iA, hS, ?_⟩
      intros x hx
      have xA := hS with x, hx
      have bound : LowerBound(A, r, upperBoundsOf(A, r, S), x)
        refine ⟨xA, upperSubset, ?_⟩
        intros b hb
        have member := upperBoundsOf.membership.forward with hb
        exact UpperBound.above with member.right, hx
      exact Infimum.greatest with hi, xA, bound
    . intros b hb bound
      have member : b ∈ upperBoundsOf(A, r, S) :=
        upperBoundsOf.membership.backward with ⟨hb, bound⟩
      exact Infimum.below with hi, member

theorem IsCompleteLattice.lattice (A r : Set)
  requires h : IsCompleteLattice(A, r)
  shows IsLattice(A, r)
proof
  apply IsLattice.of_pairs with (IsCompleteLattice.order with h)
  . intros x hx y hy
    have bounded : {x, y} ⊆ A by simp
    exact IsCompleteLattice.exists_supremum with h, bounded
  . intros x hx y hy
    have bounded : {x, y} ⊆ A by simp
    exact IsCompleteLattice.exists_infimum with h, bounded

theorem IsCompleteLattice.converse (A r : Set)
  requires h : IsCompleteLattice(A, r)
  shows IsCompleteLattice(A, converse(r, A, A))
proof
  have order := IsCompleteLattice.order with h
  apply IsCompleteLattice.of_infima with (IsPartialOrder.converse with order)
  intros S hS
  obtain ⟨s, hs⟩ := IsCompleteLattice.exists_supremum with h, hS
  refine ⟨s, Supremum.converse with hs⟩

-- The supremum and infimum of a subset

defunique supremum (A r S : Set) (s ∈ A) := Supremum(A, r, S, s)
requires complete : IsCompleteLattice(A, r)
requires hS : S ⊆ A
proof
  obtain ⟨s, hs⟩ := IsCompleteLattice.exists_supremum with complete, hS
  witness s
  refine ⟨Supremum.member with hs, hs⟩
uniqueness
  intros s sA first t tA second
  exact Supremum.unique with (IsCompleteLattice.order with complete), first,
      second

defunique infimum (A r S : Set) (i ∈ A) := Infimum(A, r, S, i)
requires complete : IsCompleteLattice(A, r)
requires hS : S ⊆ A
proof
  obtain ⟨i, hi⟩ := IsCompleteLattice.exists_infimum with complete, hS
  witness i
  refine ⟨Infimum.member with hi, hi⟩
uniqueness
  intros i iA first j jA second
  exact Infimum.unique with (IsCompleteLattice.order with complete), first,
    second

theorem supremum.member (A r S : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  shows supremum(A, r, S) ∈ A
proof
  have selected := supremum.selected with complete, hS
  exact selected.left

theorem supremum.supremum (A r S : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  shows Supremum(A, r, S, supremum(A, r, S))
proof
  have selected := supremum.selected with complete, hS
  exact selected.right

theorem supremum.upper (A r S : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  shows UpperBound(A, r, S, supremum(A, r, S))
proof
  exact Supremum.upper with (supremum.supremum with complete, hS)

theorem supremum.above (A r S x : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  requires hx : x ∈ S
  shows relates(r, x, supremum(A, r, S))
proof
  exact Supremum.above with (supremum.supremum with complete, hS), hx

theorem supremum.least (A r S b : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  requires hb : b ∈ A
  requires bound : UpperBound(A, r, S, b)
  shows relates(r, supremum(A, r, S), b)
proof
  exact Supremum.least with (supremum.supremum with complete, hS), hb, bound

theorem supremum.of_supremum (A r S s : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  requires h : Supremum(A, r, S, s)
  shows s = supremum(A, r, S)
proof
  have order := IsCompleteLattice.order with complete
  exact Supremum.unique with order, h, (supremum.supremum with complete, hS)

theorem supremum.le_iff (A r S b : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  requires hb : b ∈ A
  shows relates(r, supremum(A, r, S), b) ↔ ∀ x ∈ S, relates(r, x, b)
proof
  have order := IsCompleteLattice.order with complete
  have transitive := IsPartialOrder.transitive with order
  have supA := supremum.member with complete, hS
  constructor
  . intros below x hx
    have above := supremum.above with complete, hS, hx
    exact transitive with x, (hS with x, hx), supremum(A, r, S), supA, b, hb,
        above, below
  . intro bounds
    exact supremum.least with complete, hS, hb, ⟨hb, hS, bounds⟩

theorem infimum.member (A r S : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  shows infimum(A, r, S) ∈ A
proof
  have selected := infimum.selected with complete, hS
  exact selected.left

theorem infimum.infimum (A r S : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  shows Infimum(A, r, S, infimum(A, r, S))
proof
  have selected := infimum.selected with complete, hS
  exact selected.right

theorem infimum.lower (A r S : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  shows LowerBound(A, r, S, infimum(A, r, S))
proof
  exact Infimum.lower with (infimum.infimum with complete, hS)

theorem infimum.below (A r S x : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  requires hx : x ∈ S
  shows relates(r, infimum(A, r, S), x)
proof
  exact Infimum.below with (infimum.infimum with complete, hS), hx

theorem infimum.greatest (A r S b : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  requires hb : b ∈ A
  requires bound : LowerBound(A, r, S, b)
  shows relates(r, b, infimum(A, r, S))
proof
  exact Infimum.greatest with (infimum.infimum with complete, hS), hb, bound

theorem infimum.of_infimum (A r S i : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  requires h : Infimum(A, r, S, i)
  shows i = infimum(A, r, S)
proof
  have order := IsCompleteLattice.order with complete
  exact Infimum.unique with order, h, (infimum.infimum with complete, hS)

theorem infimum.ge_iff (A r S b : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  requires hb : b ∈ A
  shows relates(r, b, infimum(A, r, S)) ↔ ∀ x ∈ S, relates(r, b, x)
proof
  have order := IsCompleteLattice.order with complete
  have transitive := IsPartialOrder.transitive with order
  have infA := infimum.member with complete, hS
  constructor
  . intros above x hx
    have below := infimum.below with complete, hS, hx
    exact transitive with b, hb, infimum(A, r, S), infA, x, (hS with x, hx),
        above, below
  . intro bounds
    exact infimum.greatest with complete, hS, hb, ⟨hb, hS, bounds⟩

-- Monotonicity, pairs, singletons, the empty set, and the whole points

theorem supremum.monotone (A r S T : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hST : S ⊆ T
  requires hT : T ⊆ A
  shows relates(r, supremum(A, r, S), supremum(A, r, T))
proof
  have hS := Subset.transitive with hST, hT
  have supS := supremum.supremum with complete, hS
  have supT := supremum.supremum with complete, hT
  exact Supremum.monotone with hST, supS, supT

theorem infimum.antitone (A r S T : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hST : S ⊆ T
  requires hT : T ⊆ A
  shows relates(r, infimum(A, r, T), infimum(A, r, S))
proof
  have hS := Subset.transitive with hST, hT
  have infS := infimum.infimum with complete, hS
  have infT := infimum.infimum with complete, hT
  exact Infimum.antitone with hST, infS, infT

theorem supremum.pair (A r x y : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows supremum(A, r, {x, y}) = join(A, r, x, y)
proof
  have lattice := IsCompleteLattice.lattice with complete
  have bounded : {x, y} ⊆ A by simp
  have supremum := supremum.supremum with complete, bounded
  exact join.of_supremum with lattice, hx, hy, supremum

theorem infimum.pair (A r x y : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows infimum(A, r, {x, y}) = meet(A, r, x, y)
proof
  have lattice := IsCompleteLattice.lattice with complete
  have bounded : {x, y} ⊆ A by simp
  have infimum := infimum.infimum with complete, bounded
  exact meet.of_infimum with lattice, hx, hy, infimum

theorem supremum.singleton (A r x : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hx : x ∈ A
  shows supremum(A, r, {x}) = x
proof
  have order := IsCompleteLattice.order with complete
  have bounded : {x} ⊆ A by simp
  symm
  exact supremum.of_supremum with complete, bounded,
      (Supremum.singleton with order, hx)

theorem infimum.singleton (A r x : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hx : x ∈ A
  shows infimum(A, r, {x}) = x
proof
  have order := IsCompleteLattice.order with complete
  have bounded : {x} ⊆ A by simp
  symm
  exact infimum.of_infimum with complete, bounded,
      (Infimum.singleton with order, hx)

theorem supremum.empty (A r : Set)
  requires complete : IsCompleteLattice(A, r)
  shows Least(A, r, A, supremum(A, r, ∅))
proof
  have supremum := supremum.supremum with complete, (empty.subset at A)
  exact Supremum.empty_iff.forward with supremum

theorem infimum.empty (A r : Set)
  requires complete : IsCompleteLattice(A, r)
  shows Greatest(A, r, A, infimum(A, r, ∅))
proof
  have infimum := infimum.infimum with complete, (empty.subset at A)
  exact Infimum.empty_iff.forward with infimum

theorem supremum.whole (A r : Set)
  requires complete : IsCompleteLattice(A, r)
  shows Greatest(A, r, A, supremum(A, r, A))
proof
  have supremum := supremum.supremum with complete, (Subset.reflexive at A)
  exact Supremum.whole_iff.forward with supremum

theorem infimum.whole (A r : Set)
  requires complete : IsCompleteLattice(A, r)
  shows Least(A, r, A, infimum(A, r, A))
proof
  have infimum := infimum.infimum with complete, (Subset.reflexive at A)
  exact Infimum.whole_iff.forward with infimum

theorem IsCompleteLattice.bounded (A r : Set)
  requires complete : IsCompleteLattice(A, r)
  shows IsBoundedLattice(A, r, supremum(A, r, ∅), supremum(A, r, A))
proof
  have lattice := IsCompleteLattice.lattice with complete
  exact IsBoundedLattice.of_bounds with lattice, (supremum.empty with complete),
      (supremum.whole with complete)

theorem IsCompleteLattice.nonempty (A r : Set)
  requires complete : IsCompleteLattice(A, r)
  shows Nonempty(A)
proof
  exact IsBoundedLattice.nonempty with (IsCompleteLattice.bounded with complete)

theorem supremum.union2 (A r S T : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  requires hT : T ⊆ A
  shows supremum(A, r, S ∪ T) = join(A, r, supremum(A, r, S), supremum(A, r, T))
proof
  have lattice := IsCompleteLattice.lattice with complete
  have transitive := IsLattice.transitive with lattice
  have hST := union2.subset with hS, hT
  have supS := supremum.member with complete, hS
  have supT := supremum.member with complete, hT
  have joinA := join.member with lattice, supS, supT
  have sJ := join.upper_left with lattice, supS, supT
  have tJ := join.upper_right with lattice, supS, supT
  have result : Supremum(A, r, S ∪ T, join(A, r, supremum(A, r, S),
      supremum(A, r, T)))
    constructor
    . refine ⟨joinA, hST, ?_⟩
      intros x hx
      have cases := union2.membership.forward with hx
      cases cases with xS | xT
      . have above := supremum.above with complete, hS, xS
        exact transitive with x, (hS with x, xS), supremum(A, r, S), supS,
            join(A, r, supremum(A, r, S), supremum(A, r, T)), joinA, above, sJ
      . have above := supremum.above with complete, hT, xT
        exact transitive with x, (hT with x, xT), supremum(A, r, T), supT,
            join(A, r, supremum(A, r, S), supremum(A, r, T)), joinA, above, tJ
    . intros b hb bound
      have boundS := UpperBound.antitone with (union2.subset_left at S, T),
          bound
      have boundT := UpperBound.antitone with (union2.subset_right at S, T),
          bound
      have sb := supremum.least with complete, hS, hb, boundS
      have tb := supremum.least with complete, hT, hb, boundT
      exact join.least with lattice, supS, supT, hb, sb, tb
  symm
  exact supremum.of_supremum with complete, hST, result

theorem infimum.union2 (A r S T : Set)
  requires complete : IsCompleteLattice(A, r)
  requires hS : S ⊆ A
  requires hT : T ⊆ A
  shows infimum(A, r, S ∪ T) = meet(A, r, infimum(A, r, S), infimum(A, r, T))
proof
  have lattice := IsCompleteLattice.lattice with complete
  have transitive := IsLattice.transitive with lattice
  have hST := union2.subset with hS, hT
  have infS := infimum.member with complete, hS
  have infT := infimum.member with complete, hT
  have meetA := meet.member with lattice, infS, infT
  have mS := meet.lower_left with lattice, infS, infT
  have mT := meet.lower_right with lattice, infS, infT
  have result : Infimum(A, r, S ∪ T, meet(A, r, infimum(A, r, S), infimum(A,
      r, T)))
    constructor
    . refine ⟨meetA, hST, ?_⟩
      intros x hx
      have cases := union2.membership.forward with hx
      cases cases with xS | xT
      . have below := infimum.below with complete, hS, xS
        exact transitive with meet(A, r, infimum(A, r, S), infimum(A, r, T)),
            meetA, infimum(A, r, S), infS, x, (hS with x, xS), mS, below
      . have below := infimum.below with complete, hT, xT
        exact transitive with meet(A, r, infimum(A, r, S), infimum(A, r, T)),
            meetA, infimum(A, r, T), infT, x, (hT with x, xT), mT, below
    . intros b hb bound
      have boundS := LowerBound.antitone with (union2.subset_left at S, T),
          bound
      have boundT := LowerBound.antitone with (union2.subset_right at S, T),
          bound
      have bs := infimum.greatest with complete, hS, hb, boundS
      have bt := infimum.greatest with complete, hT, hb, boundT
      exact meet.greatest with lattice, infS, infT, hb, bs, bt
  symm
  exact infimum.of_infimum with complete, hST, result

-- The powerset of a set, ordered by inclusion, is a complete lattice whose
-- suprema are unions and whose infima are intersections relative to X.

def powersetOrder (X : Set) : Set := inclusionOrder(𝒫(X))

theorem powersetOrder.relates (X B C : Set)
  requires hB : B ∈ 𝒫(X)
  requires hC : C ∈ 𝒫(X)
  shows relates(powersetOrder(X), B, C) ↔ B ⊆ C
proof
  have characterization := inclusionOrder.relates with hB, hC
  simpa [powersetOrder] using characterization

theorem powersetOrder.partial (X : Set)
  shows IsPartialOrder(𝒫(X), powersetOrder(X))
proof
  have partial := inclusionOrder.partial at 𝒫(X)
  simpa [powersetOrder] using partial

def relativeIntersection (X S : Set) : Set := { x ∈ X | ∀ B ∈ S, x ∈ B }

theorem relativeIntersection.subset (X S : Set)
  shows relativeIntersection(X, S) ⊆ X
proof
  intros x hx
  have member := relativeIntersection.membership.forward with hx
  exact member.left

theorem powersetOrder.supremum (X S : Set)
  requires hS : S ⊆ 𝒫(X)
  shows Supremum(𝒫(X), powersetOrder(X), S, ⋃(S))
proof
  have unionIn : ⋃(S) ∈ 𝒫(X)
    apply powerset.membership_iff.backward
    apply union.subset
    intros B hB
    exact powerset.membership_iff.forward with (hS with B, hB)
  constructor
  . refine ⟨unionIn, hS, ?_⟩
    intros B hB
    have BIn := hS with B, hB
    apply powersetOrder.relates.backward with BIn, unionIn
    exact union.subset_of_member with hB
  . intros b hb bound
    apply powersetOrder.relates.backward with unionIn, hb
    apply union.subset
    intros B hB
    have related := UpperBound.above with bound, hB
    exact powersetOrder.relates.forward with (hS with B, hB), hb, related

theorem powersetOrder.infimum (X S : Set)
  requires hS : S ⊆ 𝒫(X)
  shows Infimum(𝒫(X), powersetOrder(X), S, relativeIntersection(X, S))
proof
  have interIn : relativeIntersection(X, S) ∈ 𝒫(X) :=
    powerset.membership_iff.backward with (relativeIntersection.subset at X, S)
  constructor
  . refine ⟨interIn, hS, ?_⟩
    intros B hB
    apply powersetOrder.relates.backward with interIn, (hS with B, hB)
    intros x hx
    have member := relativeIntersection.membership.forward with hx
    exact member.right with B, hB
  . intros b hb bound
    apply powersetOrder.relates.backward with hb, interIn
    intros x hx
    have bX := powerset.membership_iff.forward with hb
    apply relativeIntersection.membership.backward
    constructor
    . exact bX with x, hx
    . intros B hB
      have related := LowerBound.below with bound, hB
      have subset := powersetOrder.relates.forward with hb, (hS with B, hB),
          related
      exact subset with x, hx

theorem IsCompleteLattice.powerset (X : Set)
  shows IsCompleteLattice(𝒫(X), powersetOrder(X))
proof
  constructor
  . exact powersetOrder.partial at X
  . intros S hS
    refine ⟨⋃(S), powersetOrder.supremum with hS⟩

theorem powersetOrder.lattice (X : Set)
  shows IsLattice(𝒫(X), powersetOrder(X))
proof
  exact IsCompleteLattice.lattice with (IsCompleteLattice.powerset at X)

theorem powersetOrder.supremum_value (X S : Set)
  requires hS : S ⊆ 𝒫(X)
  shows supremum(𝒫(X), powersetOrder(X), S) = ⋃(S)
proof
  have complete := IsCompleteLattice.powerset at X
  symm
  exact supremum.of_supremum with complete, hS, (powersetOrder.supremum with hS)

theorem powersetOrder.infimum_value (X S : Set)
  requires hS : S ⊆ 𝒫(X)
  shows infimum(𝒫(X), powersetOrder(X), S) = relativeIntersection(X, S)
proof
  have complete := IsCompleteLattice.powerset at X
  symm
  exact infimum.of_infimum with complete, hS, (powersetOrder.infimum with hS)

theorem powersetOrder.join (X B C : Set)
  requires hB : B ∈ 𝒫(X)
  requires hC : C ∈ 𝒫(X)
  shows join(𝒫(X), powersetOrder(X), B, C) = B ∪ C
proof
  have lattice := powersetOrder.lattice at X
  have BX := powerset.membership_iff.forward with hB
  have CX := powerset.membership_iff.forward with hC
  have unionIn : B ∪ C ∈ 𝒫(X) :=
    powerset.membership_iff.backward with (union2.subset with BX, CX)
  have leftIn := powersetOrder.relates.backward with hB, unionIn,
      (union2.subset_left at B, C)
  have rightIn := powersetOrder.relates.backward with hC, unionIn,
      (union2.subset_right at B, C)
  have supremum : Supremum(𝒫(X), powersetOrder(X), {B, C}, B ∪ C)
    apply Supremum.of_pair with hB, hC, unionIn, leftIn, rightIn
    intros D hD BD CD
    have BDsubset := powersetOrder.relates.forward with hB, hD, BD
    have CDsubset := powersetOrder.relates.forward with hC, hD, CD
    apply powersetOrder.relates.backward with unionIn, hD
    exact union2.subset with BDsubset, CDsubset
  symm
  exact join.of_supremum with lattice, hB, hC, supremum

theorem powersetOrder.meet (X B C : Set)
  requires hB : B ∈ 𝒫(X)
  requires hC : C ∈ 𝒫(X)
  shows meet(𝒫(X), powersetOrder(X), B, C) = B ∩ C
proof
  have lattice := powersetOrder.lattice at X
  have BX := powerset.membership_iff.forward with hB
  have interIn : B ∩ C ∈ 𝒫(X) :=
    powerset.membership_iff.backward with (Subset.transitive with (intersection.subset_left at B, C), BX)
  have leftIn := powersetOrder.relates.backward with interIn, hB,
      (intersection.subset_left at B, C)
  have rightIn := powersetOrder.relates.backward with interIn, hC,
      (intersection.subset_right at B, C)
  have infimum : Infimum(𝒫(X), powersetOrder(X), {B, C}, B ∩ C)
    apply Infimum.of_pair with hB, hC, interIn, leftIn, rightIn
    intros D hD DB DC
    have DBsubset := powersetOrder.relates.forward with hD, hB, DB
    have DCsubset := powersetOrder.relates.forward with hD, hC, DC
    apply powersetOrder.relates.backward with hD, interIn
    exact intersection.greatest with DBsubset, DCsubset
  symm
  exact meet.of_infimum with lattice, hB, hC, infimum

theorem powersetOrder.bounded (X : Set)
  shows IsBoundedLattice(𝒫(X), powersetOrder(X), ∅, X)
proof
  have lattice := powersetOrder.lattice at X
  have emptyIn := powerset.empty_member at X
  have selfIn := powerset.self at X
  apply IsBoundedLattice.of_bounds with lattice
  . constructor
    . exact emptyIn
    . refine ⟨emptyIn, Subset.reflexive at 𝒫(X), ?_⟩
      intros B hB
      exact powersetOrder.relates.backward with emptyIn, hB, (empty.subset at B)
  . constructor
    . exact selfIn
    . refine ⟨selfIn, Subset.reflexive at 𝒫(X), ?_⟩
      intros B hB
      exact powersetOrder.relates.backward with hB, selfIn,
          (powerset.membership_iff.forward with hB)