Nuprl Lemma : rat-sign-change-list_wf
∀[f:(ℤ × ℕ+) ⟶ (ℤ × ℕ+)]. ∀[a,b:ℤ × ℕ+]. ∀[L:(ℤ × ℕ+) List]. (rat-sign-change-list(f;a;b;L) ∈ ℙ)
Proof
Error : references
Latex:
\mforall{}[f:(\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}) {}\mrightarrow{} (\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{})]. \mforall{}[a,b:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}]. \mforall{}[L:(\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}) List]. (rat-sign-change-list(f;a;b;L) \mmember{} \mBbbP{})
Date html generated:
2019_11_06-PM-00_35_06
Last ObjectModification:
2019_01_16-PM-04_16_28
Theory : reals
Home
Index