Grace/Cumulus/Lattice/Bounds.g17

Open in Workbench Download source

Imports

Set.Order

Declarations

Source

1-- Suprema and infima of subsets of an ordered set, and order duality2-- 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.Bounds8import Set.Order910-- A supremum is a least upper bound; an infimum is a greatest lower bound.11predicate Supremum (A r S s : Set) :=12  UpperBound(A, r, S, s) ∧ (∀ b ∈ A, UpperBound(A, r, S, b) → relates(r, s, b))13predicate Infimum (A r S i : Set) :=14  LowerBound(A, r, S, i) ∧ (∀ b ∈ A, LowerBound(A, r, S, b) → relates(r, b, i))1516-- Projections of the bound predicates1718theorem UpperBound.member (A r S a : Set)19  requires h : UpperBound(A, r, S, a)20  shows a ∈ A21proof22  simp [UpperBound]2324theorem UpperBound.subset (A r S a : Set)25  requires h : UpperBound(A, r, S, a)26  shows S ⊆ A27proof28  simp [UpperBound]2930theorem UpperBound.above (A r S a x : Set)31  requires h : UpperBound(A, r, S, a)32  requires hx : x ∈ S33  shows relates(r, x, a)34proof35  rcases h with ⟨member, bounded, above⟩36  exact above with x, hx3738theorem LowerBound.member (A r S a : Set)39  requires h : LowerBound(A, r, S, a)40  shows a ∈ A41proof42  simp [LowerBound]4344theorem LowerBound.subset (A r S a : Set)45  requires h : LowerBound(A, r, S, a)46  shows S ⊆ A47proof48  simp [LowerBound]4950theorem LowerBound.below (A r S a x : Set)51  requires h : LowerBound(A, r, S, a)52  requires hx : x ∈ S53  shows relates(r, a, x)54proof55  rcases h with ⟨member, bounded, below⟩56  exact below with x, hx5758theorem Least.member (A r S a : Set)59  requires h : Least(A, r, S, a)60  shows a ∈ S61proof62  simp [Least]6364theorem Least.lower (A r S a : Set)65  requires h : Least(A, r, S, a)66  shows LowerBound(A, r, S, a)67proof68  simp [Least]6970theorem Least.below (A r S a x : Set)71  requires h : Least(A, r, S, a)72  requires hx : x ∈ S73  shows relates(r, a, x)74proof75  have lower := Least.lower with h76  exact LowerBound.below with lower, hx7778theorem Greatest.member (A r S a : Set)79  requires h : Greatest(A, r, S, a)80  shows a ∈ S81proof82  simp [Greatest]8384theorem Greatest.upper (A r S a : Set)85  requires h : Greatest(A, r, S, a)86  shows UpperBound(A, r, S, a)87proof88  simp [Greatest]8990theorem Greatest.above (A r S a x : Set)91  requires h : Greatest(A, r, S, a)92  requires hx : x ∈ S93  shows relates(r, x, a)94proof95  have upper := Greatest.upper with h96  exact UpperBound.above with upper, hx9798-- Bounds of the empty set, of subsets, and of pairs99100theorem UpperBound.empty (A r a : Set)101  requires ha : a ∈ A102  shows UpperBound(A, r, ∅, a)103proof104  refine ⟨ha, empty.subset at A, ?_⟩105  intros x hx106  exfalso107  exact set.empty with hx108109theorem LowerBound.empty (A r a : Set)110  requires ha : a ∈ A111  shows LowerBound(A, r, ∅, a)112proof113  refine ⟨ha, empty.subset at A, ?_⟩114  intros x hx115  exfalso116  exact set.empty with hx117118theorem UpperBound.antitone (A r S T a : Set)119  requires hST : S ⊆ T120  requires h : UpperBound(A, r, T, a)121  shows UpperBound(A, r, S, a)122proof123  rcases h with ⟨member, bounded, above⟩124  refine ⟨member, (Subset.transitive with hST, bounded), ?_⟩125  intros x hx126  exact above with x, (hST with x, hx)127128theorem LowerBound.antitone (A r S T a : Set)129  requires hST : S ⊆ T130  requires h : LowerBound(A, r, T, a)131  shows LowerBound(A, r, S, a)132proof133  rcases h with ⟨member, bounded, below⟩134  refine ⟨member, (Subset.transitive with hST, bounded), ?_⟩135  intros x hx136  exact below with x, (hST with x, hx)137138theorem UpperBound.raise (A r S a b : Set)139  requires order : IsPartialOrder(A, r)140  requires h : UpperBound(A, r, S, a)141  requires hb : b ∈ A142  requires hab : relates(r, a, b)143  shows UpperBound(A, r, S, b)144proof145  have transitive := IsPartialOrder.transitive with order146  rcases h with ⟨member, bounded, above⟩147  refine ⟨hb, bounded, ?_⟩148  intros x hx149  have xA := bounded with x, hx150  exact transitive with x, xA, a, member, b, hb, (above with x, hx), hab151152theorem LowerBound.lower (A r S a b : Set)153  requires order : IsPartialOrder(A, r)154  requires h : LowerBound(A, r, S, a)155  requires hb : b ∈ A156  requires hba : relates(r, b, a)157  shows LowerBound(A, r, S, b)158proof159  have transitive := IsPartialOrder.transitive with order160  rcases h with ⟨member, bounded, below⟩161  refine ⟨hb, bounded, ?_⟩162  intros x hx163  have xA := bounded with x, hx164  exact transitive with b, hb, a, member, x, xA, hba, (below with x, hx)165166theorem UpperBound.singleton (A r x : Set)167  requires order : IsPartialOrder(A, r)168  requires hx : x ∈ A169  shows UpperBound(A, r, {x}, x)170proof171  have reflexive := IsPartialOrder.reflexive with order172  have bounded : {x} ⊆ A by simp173  refine ⟨hx, bounded, ?_⟩174  intros y hy175  have equal := singleton.membership.forward with hy176  rw equal177  exact reflexive with x, hx178179theorem LowerBound.singleton (A r x : Set)180  requires order : IsPartialOrder(A, r)181  requires hx : x ∈ A182  shows LowerBound(A, r, {x}, x)183proof184  have reflexive := IsPartialOrder.reflexive with order185  have bounded : {x} ⊆ A by simp186  refine ⟨hx, bounded, ?_⟩187  intros y hy188  have equal := singleton.membership.forward with hy189  rw equal190  exact reflexive with x, hx191192theorem UpperBound.pair (A r x y a : Set)193  requires hx : x ∈ A194  requires hy : y ∈ A195  requires ha : a ∈ A196  requires hxa : relates(r, x, a)197  requires hya : relates(r, y, a)198  shows UpperBound(A, r, {x, y}, a)199proof200  have bounded : {x, y} ⊆ A by simp201  refine ⟨ha, bounded, ?_⟩202  intros z hz203  have cases := pair.membership.forward with hz204  cases cases with zx | zy205  . rw zx206    exact hxa207  . rw zy208    exact hya209210theorem LowerBound.pair (A r x y a : Set)211  requires hx : x ∈ A212  requires hy : y ∈ A213  requires ha : a ∈ A214  requires hax : relates(r, a, x)215  requires hay : relates(r, a, y)216  shows LowerBound(A, r, {x, y}, a)217proof218  have bounded : {x, y} ⊆ A by simp219  refine ⟨ha, bounded, ?_⟩220  intros z hz221  have cases := pair.membership.forward with hz222  cases cases with zx | zy223  . rw zx224    exact hax225  . rw zy226    exact hay227228theorem UpperBound.pair_left (A r x y a : Set)229  requires h : UpperBound(A, r, {x, y}, a)230  shows relates(r, x, a)231proof232  exact UpperBound.above with h, (pair.left at x, y)233234theorem UpperBound.pair_right (A r x y a : Set)235  requires h : UpperBound(A, r, {x, y}, a)236  shows relates(r, y, a)237proof238  exact UpperBound.above with h, (pair.right at x, y)239240theorem LowerBound.pair_left (A r x y a : Set)241  requires h : LowerBound(A, r, {x, y}, a)242  shows relates(r, a, x)243proof244  exact LowerBound.below with h, (pair.left at x, y)245246theorem LowerBound.pair_right (A r x y a : Set)247  requires h : LowerBound(A, r, {x, y}, a)248  shows relates(r, a, y)249proof250  exact LowerBound.below with h, (pair.right at x, y)251252-- Projections of suprema and infima253254theorem Supremum.upper (A r S s : Set)255  requires h : Supremum(A, r, S, s)256  shows UpperBound(A, r, S, s)257proof258  simp [Supremum]259260theorem Supremum.least (A r S s b : Set)261  requires h : Supremum(A, r, S, s)262  requires hb : b ∈ A263  requires bound : UpperBound(A, r, S, b)264  shows relates(r, s, b)265proof266  rcases h with ⟨upper, least⟩267  exact least with b, hb, bound268269theorem Supremum.member (A r S s : Set)270  requires h : Supremum(A, r, S, s)271  shows s ∈ A272proof273  exact UpperBound.member with (Supremum.upper with h)274275theorem Supremum.subset (A r S s : Set)276  requires h : Supremum(A, r, S, s)277  shows S ⊆ A278proof279  exact UpperBound.subset with (Supremum.upper with h)280281theorem Supremum.above (A r S s x : Set)282  requires h : Supremum(A, r, S, s)283  requires hx : x ∈ S284  shows relates(r, x, s)285proof286  exact UpperBound.above with (Supremum.upper with h), hx287288theorem Infimum.lower (A r S i : Set)289  requires h : Infimum(A, r, S, i)290  shows LowerBound(A, r, S, i)291proof292  simp [Infimum]293294theorem Infimum.greatest (A r S i b : Set)295  requires h : Infimum(A, r, S, i)296  requires hb : b ∈ A297  requires bound : LowerBound(A, r, S, b)298  shows relates(r, b, i)299proof300  rcases h with ⟨lower, greatest⟩301  exact greatest with b, hb, bound302303theorem Infimum.member (A r S i : Set)304  requires h : Infimum(A, r, S, i)305  shows i ∈ A306proof307  exact LowerBound.member with (Infimum.lower with h)308309theorem Infimum.subset (A r S i : Set)310  requires h : Infimum(A, r, S, i)311  shows S ⊆ A312proof313  exact LowerBound.subset with (Infimum.lower with h)314315theorem Infimum.below (A r S i x : Set)316  requires h : Infimum(A, r, S, i)317  requires hx : x ∈ S318  shows relates(r, i, x)319proof320  exact LowerBound.below with (Infimum.lower with h), hx321322-- Uniqueness323324theorem Supremum.unique (A r S s t : Set)325  requires order : IsPartialOrder(A, r)326  requires hs : Supremum(A, r, S, s)327  requires ht : Supremum(A, r, S, t)328  shows s = t329proof330  have antisymmetric := IsPartialOrder.antisymmetric with order331  have sA := Supremum.member with hs332  have tA := Supremum.member with ht333  have st := Supremum.least with hs, tA, (Supremum.upper with ht)334  have ts := Supremum.least with ht, sA, (Supremum.upper with hs)335  exact antisymmetric with s, sA, t, tA, st, ts336337theorem Infimum.unique (A r S i j : Set)338  requires order : IsPartialOrder(A, r)339  requires hi : Infimum(A, r, S, i)340  requires hj : Infimum(A, r, S, j)341  shows i = j342proof343  have antisymmetric := IsPartialOrder.antisymmetric with order344  have iA := Infimum.member with hi345  have jA := Infimum.member with hj346  have ji := Infimum.greatest with hi, jA, (Infimum.lower with hj)347  have ij := Infimum.greatest with hj, iA, (Infimum.lower with hi)348  exact antisymmetric with i, iA, j, jA, ij, ji349350-- Greatest elements are suprema, and a supremum that belongs to the set351-- is its greatest element.352353theorem Greatest.supremum (A r S g : Set)354  requires h : Greatest(A, r, S, g)355  shows Supremum(A, r, S, g)356proof357  rcases h with ⟨member, upper⟩358  constructor359  . exact upper360  . intros b hb bound361    exact UpperBound.above with bound, member362363theorem Least.infimum (A r S l : Set)364  requires h : Least(A, r, S, l)365  shows Infimum(A, r, S, l)366proof367  rcases h with ⟨member, lower⟩368  constructor369  . exact lower370  . intros b hb bound371    exact LowerBound.below with bound, member372373theorem Supremum.greatest_of_member (A r S s : Set)374  requires h : Supremum(A, r, S, s)375  requires hs : s ∈ S376  shows Greatest(A, r, S, s)377proof378  refine ⟨hs, Supremum.upper with h⟩379380theorem Infimum.least_of_member (A r S i : Set)381  requires h : Infimum(A, r, S, i)382  requires hi : i ∈ S383  shows Least(A, r, S, i)384proof385  refine ⟨hi, Infimum.lower with h⟩386387-- The empty set and the whole points388389theorem Supremum.empty_iff (A r s : Set)390  shows Supremum(A, r, ∅, s) ↔ Least(A, r, A, s)391proof392  constructor393  . intro h394    have sA := Supremum.member with h395    constructor396    . exact sA397    . refine ⟨sA, Subset.reflexive at A, ?_⟩398      intros x hx399      exact Supremum.least with h, hx, (UpperBound.empty at A, r, x with hx)400  . intro h401    rcases h with ⟨sA, _, _, below⟩402    constructor403    . exact UpperBound.empty with sA404    . intros b hb bound405      exact below with b, hb406407theorem Infimum.empty_iff (A r i : Set)408  shows Infimum(A, r, ∅, i) ↔ Greatest(A, r, A, i)409proof410  constructor411  . intro h412    have iA := Infimum.member with h413    constructor414    . exact iA415    . refine ⟨iA, Subset.reflexive at A, ?_⟩416      intros x hx417      exact Infimum.greatest with h, hx, (LowerBound.empty at A, r, x with hx)418  . intro h419    rcases h with ⟨iA, _, _, above⟩420    constructor421    . exact LowerBound.empty with iA422    . intros b hb bound423      exact above with b, hb424425theorem Supremum.whole_iff (A r s : Set)426  shows Supremum(A, r, A, s) ↔ Greatest(A, r, A, s)427proof428  constructor429  . intro h430    exact Supremum.greatest_of_member with h, (Supremum.member with h)431  . intro h432    exact Greatest.supremum with h433434theorem Infimum.whole_iff (A r i : Set)435  shows Infimum(A, r, A, i) ↔ Least(A, r, A, i)436proof437  constructor438  . intro h439    exact Infimum.least_of_member with h, (Infimum.member with h)440  . intro h441    exact Least.infimum with h442443-- Singletons and pairs444445theorem Supremum.singleton (A r x : Set)446  requires order : IsPartialOrder(A, r)447  requires hx : x ∈ A448  shows Supremum(A, r, {x}, x)449proof450  constructor451  . exact UpperBound.singleton with order, hx452  . intros b hb bound453    exact UpperBound.above with bound, (singleton.self at x)454455theorem Infimum.singleton (A r x : Set)456  requires order : IsPartialOrder(A, r)457  requires hx : x ∈ A458  shows Infimum(A, r, {x}, x)459proof460  constructor461  . exact LowerBound.singleton with order, hx462  . intros b hb bound463    exact LowerBound.below with bound, (singleton.self at x)464465theorem Supremum.of_pair (A r x y s : Set)466  requires hx : x ∈ A467  requires hy : y ∈ A468  requires hs : s ∈ A469  requires hxs : relates(r, x, s)470  requires hys : relates(r, y, s)471  requires least :472    ∀ b ∈ A, relates(r, x, b) → relates(r, y, b) → relates(r, s, b)473  shows Supremum(A, r, {x, y}, s)474proof475  constructor476  . exact UpperBound.pair with hx, hy, hs, hxs, hys477  . intros b hb bound478    have xb := UpperBound.pair_left with bound479    have yb := UpperBound.pair_right with bound480    exact least with b, hb, xb, yb481482theorem Infimum.of_pair (A r x y i : Set)483  requires hx : x ∈ A484  requires hy : y ∈ A485  requires hi : i ∈ A486  requires hix : relates(r, i, x)487  requires hiy : relates(r, i, y)488  requires greatest :489    ∀ b ∈ A, relates(r, b, x) → relates(r, b, y) → relates(r, b, i)490  shows Infimum(A, r, {x, y}, i)491proof492  constructor493  . exact LowerBound.pair with hx, hy, hi, hix, hiy494  . intros b hb bound495    have bx := LowerBound.pair_left with bound496    have byBound := LowerBound.pair_right with bound497    exact greatest with b, hb, bx, byBound498499theorem Supremum.pair_left (A r x y s : Set)500  requires h : Supremum(A, r, {x, y}, s)501  shows relates(r, x, s)502proof503  exact UpperBound.pair_left with (Supremum.upper with h)504505theorem Supremum.pair_right (A r x y s : Set)506  requires h : Supremum(A, r, {x, y}, s)507  shows relates(r, y, s)508proof509  exact UpperBound.pair_right with (Supremum.upper with h)510511theorem Supremum.pair_least (A r x y s b : Set)512  requires h : Supremum(A, r, {x, y}, s)513  requires hb : b ∈ A514  requires hxb : relates(r, x, b)515  requires hyb : relates(r, y, b)516  shows relates(r, s, b)517proof518  have bounded := Supremum.subset with h519  have xA := bounded with x, (pair.left at x, y)520  have yA := bounded with y, (pair.right at x, y)521  have bound := UpperBound.pair with xA, yA, hb, hxb, hyb522  exact Supremum.least with h, hb, bound523524theorem Infimum.pair_left (A r x y i : Set)525  requires h : Infimum(A, r, {x, y}, i)526  shows relates(r, i, x)527proof528  exact LowerBound.pair_left with (Infimum.lower with h)529530theorem Infimum.pair_right (A r x y i : Set)531  requires h : Infimum(A, r, {x, y}, i)532  shows relates(r, i, y)533proof534  exact LowerBound.pair_right with (Infimum.lower with h)535536theorem Infimum.pair_greatest (A r x y i b : Set)537  requires h : Infimum(A, r, {x, y}, i)538  requires hb : b ∈ A539  requires hbx : relates(r, b, x)540  requires hby : relates(r, b, y)541  shows relates(r, b, i)542proof543  have bounded := Infimum.subset with h544  have xA := bounded with x, (pair.left at x, y)545  have yA := bounded with y, (pair.right at x, y)546  have bound := LowerBound.pair with xA, yA, hb, hbx, hby547  exact Infimum.greatest with h, hb, bound548549-- Monotonicity in the set550551theorem Supremum.monotone (A r S T s t : Set)552  requires hST : S ⊆ T553  requires hs : Supremum(A, r, S, s)554  requires ht : Supremum(A, r, T, t)555  shows relates(r, s, t)556proof557  have tA := Supremum.member with ht558  have bound := UpperBound.antitone with hST, (Supremum.upper with ht)559  exact Supremum.least with hs, tA, bound560561theorem Infimum.antitone (A r S T i j : Set)562  requires hST : S ⊆ T563  requires hi : Infimum(A, r, S, i)564  requires hj : Infimum(A, r, T, j)565  shows relates(r, j, i)566proof567  have jA := Infimum.member with hj568  have bound := LowerBound.antitone with hST, (Infimum.lower with hj)569  exact Infimum.greatest with hi, jA, bound570571-- Duality: the converse of an order exchanges the two notions.572573theorem IsPartialOrder.converse (A r : Set)574  requires order : IsPartialOrder(A, r)575  shows IsPartialOrder(A, converse(r, A, A))576proof577  have reflexive := IsPartialOrder.reflexive with order578  have transitive := IsPartialOrder.transitive with order579  have antisymmetric := IsPartialOrder.antisymmetric with order580  constructor581  . constructor582    . exact converse.relation at r, A, A583    . constructor584      . intros x hx585        exact converse.relates with hx, hx, (reflexive with x, hx)586      . intros x hx y hy z hz xy yz587        have yx := converse.reflects with xy588        have zy := converse.reflects with yz589        have zx := transitive with z, hz, y, hy, x, hx, zy, yx590        exact converse.relates with hz, hx, zx591  . intros x hx y hy xy yx592    have yxR := converse.reflects with xy593    have xyR := converse.reflects with yx594    exact antisymmetric with x, hx, y, hy, xyR, yxR595596theorem UpperBound.converse (A r S a : Set)597  requires h : UpperBound(A, r, S, a)598  shows LowerBound(A, converse(r, A, A), S, a)599proof600  rcases h with ⟨member, bounded, above⟩601  refine ⟨member, bounded, ?_⟩602  intros x hx603  have xA := bounded with x, hx604  exact converse.relates with xA, member, (above with x, hx)605606theorem LowerBound.converse (A r S a : Set)607  requires h : LowerBound(A, r, S, a)608  shows UpperBound(A, converse(r, A, A), S, a)609proof610  rcases h with ⟨member, bounded, below⟩611  refine ⟨member, bounded, ?_⟩612  intros x hx613  have xA := bounded with x, hx614  exact converse.relates with member, xA, (below with x, hx)615616theorem UpperBound.of_converse (A r S a : Set)617  requires h : UpperBound(A, converse(r, A, A), S, a)618  shows LowerBound(A, r, S, a)619proof620  rcases h with ⟨member, bounded, above⟩621  refine ⟨member, bounded, ?_⟩622  intros x hx623  exact converse.reflects with (above with x, hx)624625theorem LowerBound.of_converse (A r S a : Set)626  requires h : LowerBound(A, converse(r, A, A), S, a)627  shows UpperBound(A, r, S, a)628proof629  rcases h with ⟨member, bounded, below⟩630  refine ⟨member, bounded, ?_⟩631  intros x hx632  exact converse.reflects with (below with x, hx)633634theorem Supremum.converse (A r S s : Set)635  requires h : Supremum(A, r, S, s)636  shows Infimum(A, converse(r, A, A), S, s)637proof638  have sA := Supremum.member with h639  constructor640  . exact UpperBound.converse with (Supremum.upper with h)641  . intros b hb bound642    have upper := LowerBound.of_converse with bound643    have sb := Supremum.least with h, hb, upper644    exact converse.relates with sA, hb, sb645646theorem Infimum.converse (A r S i : Set)647  requires h : Infimum(A, r, S, i)648  shows Supremum(A, converse(r, A, A), S, i)649proof650  have iA := Infimum.member with h651  constructor652  . exact LowerBound.converse with (Infimum.lower with h)653  . intros b hb bound654    have lower := UpperBound.of_converse with bound655    have bi := Infimum.greatest with h, hb, lower656    exact converse.relates with hb, iA, bi657658theorem Supremum.of_converse (A r S s : Set)659  requires h : Supremum(A, converse(r, A, A), S, s)660  shows Infimum(A, r, S, s)661proof662  have sA := Supremum.member with h663  constructor664  . exact UpperBound.of_converse with (Supremum.upper with h)665  . intros b hb bound666    have upper := LowerBound.converse with bound667    have sb := Supremum.least with h, hb, upper668    exact converse.reflects with sb669670theorem Infimum.of_converse (A r S i : Set)671  requires h : Infimum(A, converse(r, A, A), S, i)672  shows Supremum(A, r, S, i)673proof674  have iA := Infimum.member with h675  constructor676  . exact LowerBound.of_converse with (Infimum.lower with h)677  . intros b hb bound678    have lower := UpperBound.converse with bound679    have bi := Infimum.greatest with h, hb, lower680    exact converse.reflects with bi681682theorem Least.converse (A r S a : Set)683  requires h : Least(A, r, S, a)684  shows Greatest(A, converse(r, A, A), S, a)685proof686  rcases h with ⟨member, lower⟩687  refine ⟨member, LowerBound.converse with lower⟩688689theorem Greatest.converse (A r S a : Set)690  requires h : Greatest(A, r, S, a)691  shows Least(A, converse(r, A, A), S, a)692proof693  rcases h with ⟨member, upper⟩694  refine ⟨member, UpperBound.converse with upper⟩695