src/HOL/Algebra/Lattice.thy
 changeset 19286 83404ccd270a parent 16417 9bc16273c2d4 child 19783 82f365a14960
equal inserted replaced
19285:dac2c8014253 19286:83404ccd270a
`    27     and trans [trans]:`
`    27     and trans [trans]:`
`    28                   "[| x \<sqsubseteq> y; y \<sqsubseteq> z;`
`    28                   "[| x \<sqsubseteq> y; y \<sqsubseteq> z;`
`    29                    x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"`
`    29                    x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"`
`    30 `
`    30 `
`    31 constdefs (structure L)`
`    31 constdefs (structure L)`
`    32   less :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)`
`    32   lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)`
`    33   "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"`
`    33   "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"`
`    34 `
`    34 `
`    35   -- {* Upper and lower bounds of a set. *}`
`    35   -- {* Upper and lower bounds of a set. *}`
`    36   Upper :: "[_, 'a set] => 'a set"`
`    36   Upper :: "[_, 'a set] => 'a set"`
`    37   "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>`
`    37   "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>`