Menu
▾
▴
#384 Inference rules for bounds
Jean-Paul Bodeveix requests new inference rules that could be used, in particular, to prove the WD conditions of min and max: ∀ S · finite(S ∩ ℕ) ⇒ (∃ b · ∀ x · x ∈ S ⇒ b ≥ x) and ∀ S · finite(S ∖ ℕ) ⇒ (∃ b · ∀ x · x ∈ S ⇒ b ≤ x).
Note that if S is finite, there are already rules to prove the existence of a bound (FIN_L_{UPPER,LOWER}_BOUND_{L,R}).
