equal
deleted
inserted
replaced
133 v :: "'a" |
133 v :: "'a" |
134 assumes |
134 assumes |
135 Y_ss "Y <= P" |
135 Y_ss "Y <= P" |
136 defines |
136 defines |
137 intY1_def "intY1 == interval r (lub Y cl) (Top cl)" |
137 intY1_def "intY1 == interval r (lub Y cl) (Top cl)" |
138 v_def "v == glb {x. ((lam x: intY1. f x) x, x): induced intY1 r & x: intY1} |
138 v_def "v == glb {x. ((%x: intY1. f x) x, x): induced intY1 r & x: intY1} |
139 (| pset=intY1, order=induced intY1 r|)" |
139 (| pset=intY1, order=induced intY1 r|)" |
140 |
140 |
141 end |
141 end |