Nuprl Lemma : interval-fun_wf
∀[I,J:Interval]. ∀[f:I ⟶ℝ]. (interval-fun(I;J;x.f[x]) ∈ ℙ)
Proof
Definitions occuring in Statement :
interval-fun: interval-fun(I;J;x.f[x]),
rfun: I ⟶ℝ,
interval: Interval,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
interval-fun: interval-fun(I;J;x.f[x]),
prop: ℙ,
and: P ∧ Q,
all: ∀x:A. B[x],
so_apply: x[s],
rfun: I ⟶ℝ,
uimplies: b supposing a
Latex:
\mforall{}[I,J:Interval]. \mforall{}[f:I {}\mrightarrow{}\mBbbR{}]. (interval-fun(I;J;x.f[x]) \mmember{} \mBbbP{})
Date html generated:
2020_05_20-PM-00_25_11
Last ObjectModification:
2019_12_05-PM-05_48_27
Theory : reals
Home
Index