Conditionally complete linear order structure on ℕ
#
In this file we
- define a
ConditionallyCompleteLinearOrderBot
structure onℕ
; - prove a few lemmas about
iSup
/iInf
/Set.iUnion
/Set.iInter
and natural numbers.
This instance is necessary, otherwise the lattice operations would be derived via
ConditionallyCompleteLinearOrderBot
and marked as noncomputable.