Grace/Cumulus/Lattice/Linear.g17

Open in Workbench Download source

Imports

LinearLattice · DistribLattice

Declarations

• LinearOrder.lattice_of theorem derivation
• LinearOrder.distributive_of instance derivation
• LinearOrder.modular_of theorem derivation
• LinearOrder.dual theorem derivation
• sup_eq_left_or_right theorem derivation
• inf_eq_left_or_right theorem derivation
• sup_mem_pair theorem derivation
• inf_mem_pair theorem derivation

Source

1-- Linear orders as distributive lattices, bundled2-- 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.Linear8import LinearLattice9import DistribLattice1011-- A linear order is a lattice: the join of two elements is the larger and12-- the meet the smaller, and the lattice is distributive.13theorem LinearOrder.lattice_of (P : Set)14  requires linear : LinearOrder(P)15  shows Lattice(P)16proof17  unfold Join.Lattice18  exact IsLinearOrder.lattice with (LinearOrder.unbundled with linear)1920instance LinearOrder.distributive_of (P : Set)21  requires linear : LinearOrder(P)22  shows DistributiveLattice(P)23proof24  unfold DistribLattice.DistributiveLattice25  exact IsLinearOrder.distributive with (LinearOrder.unbundled with linear)2627theorem LinearOrder.modular_of (P : Set)28  requires linear : LinearOrder(P)29  shows ModularLattice(P)30proof31  unfold DistribLattice.ModularLattice32  exact IsLinearOrder.modular with (LinearOrder.unbundled with linear)3334notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis LinearOrder(P) for P.points35notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis LinearOrder(P) for P.points3637theorem LinearOrder.dual (P : Set)38  requires linear : LinearOrder(P)39  shows LinearOrder(dual(P))40proof41  unfold dual42  apply LinearOrder.mk43  exact IsLinearOrder.converse with (LinearOrder.unbundled with linear)4445section LinearLaws46variable (P : Set)47hypothesis linear : LinearOrder(P)4849theorem sup_eq_left_or_right (a b ∈ points(P))50  shows a ⊔ b = a ∨ a ⊔ b = b51proof52  rw sup.join53  exact IsLinearOrder.join_cases with *5455theorem inf_eq_left_or_right (a b ∈ points(P))56  shows a ⊓ b = a ∨ a ⊓ b = b57proof58  rw inf.meet59  exact IsLinearOrder.meet_cases with *6061theorem sup_mem_pair (a b ∈ points(P))62  shows a ⊔ b ∈ {a, b}63proof64  rw sup.join65  exact IsLinearOrder.join_member_pair with *6667theorem inf_mem_pair (a b ∈ points(P))68  shows a ⊓ b ∈ {a, b}69proof70  rw inf.meet71  exact IsLinearOrder.meet_member_pair with *7273end LinearLaws74