Entry	Value
Package Name	natural-order-min-max-def
Count	3
Theorems	MAX : !m n. MAX m n = (if m <= n then n else m) MIN : !m n. MIN m n = (if m <= n then m else n) MINIMAL : !p. (?n. p n) <=> p ((minimal) p) /\ (!m. m < (minimal) p ==> ~p m)

Back to main package page