Nuprl Definition : altfan
This is an alternate statement of the fan theorem for "detachable" bars
where we use the type n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹 for the "set" of nodes.
Since we are using 𝔹 (boolean) instead of ⌜ℙ⌝, the decidablity is built in.
Also, the use of ⌜n ∈ ℕ⌝ and ⌜ℕn ⟶ T⌝ to represent finite sequences
turns out to be nicer than using ⌜T List⌝.⋅
Fan(T) == ∀X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹. (bar(X) ⇒ uniformBar(X))
Definitions occuring in Statement :
altubar: uniformBar(X),
altbar: bar(X),
int_seg: {i..j-},
nat: ℕ,
bool: 𝔹,
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
altubar: uniformBar(X),
altbar: bar(X),
implies: P ⇒ Q,
bool: 𝔹,
natural_number: $n,
int_seg: {i..j-},
function: x:A ⟶ B[x],
nat: ℕ,
all: ∀x:A. B[x]
FDL editor aliases :
altfan
Latex:
Fan(T) == \mforall{}X:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} \mBbbB{}. (bar(X) {}\mRightarrow{} uniformBar(X))
Date html generated:
2019_06_20-PM-02_46_01
Last ObjectModification:
2019_06_07-PM-00_00_53
Theory : fan-theorem
Home
Index