Nuprl Lemma : u-almost-full-filter
∀A,B:ℕ ⟶ ℙ.
((u-almost-full(n.A[n]) ⇒ u-almost-full(n.B[n]) ⇒ u-almost-full(n.A[n] ∧ B[n]))
∧ ((∀n:ℕ. (A[n] ⇒ B[n])) ⇒ u-almost-full(n.A[n]) ⇒ u-almost-full(n.B[n]))
∧ u-almost-full(n.True))
Proof
Definitions occuring in Statement :
u-almost-full: u-almost-full(n.A[n]),
nat: ℕ,
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
true: True,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
and: P ∧ Q,
cand: A c∧ B,
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s],
u-almost-full: u-almost-full(n.A[n]),
strict-inc: StrictInc,
exists: ∃x:A. B[x],
guard: {T},
nat: ℕ,
le: A ≤ B,
less_than': less_than'(a;b),
false: False,
not: ¬A,
true: True,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uimplies: b supposing a
Lemmas referenced :
u-almost-full_wf,
nat_wf,
all_wf,
intuitionistic-pigeonhole,
strict-inc_wf,
implies-quotient-true,
exists_wf,
true_wf,
equiv_rel_true,
false_wf,
le_wf,
quotient-member-eq
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality,
applyEquality,
hypothesisEquality,
hypothesis,
independent_pairFormation,
independent_functionElimination,
because_Cache,
functionEquality,
cumulativity,
universeEquality,
dependent_functionElimination,
setElimination,
rename,
productElimination,
dependent_pairFormation,
introduction,
dependent_pairEquality,
dependent_set_memberEquality,
natural_numberEquality,
axiomEquality,
independent_isectElimination
Latex:
\mforall{}A,B:\mBbbN{} {}\mrightarrow{} \mBbbP{}.
((u-almost-full(n.A[n]) {}\mRightarrow{} u-almost-full(n.B[n]) {}\mRightarrow{} u-almost-full(n.A[n] \mwedge{} B[n]))
\mwedge{} ((\mforall{}n:\mBbbN{}. (A[n] {}\mRightarrow{} B[n])) {}\mRightarrow{} u-almost-full(n.A[n]) {}\mRightarrow{} u-almost-full(n.B[n]))
\mwedge{} u-almost-full(n.True))
Date html generated:
2016_05_14-PM-09_48_55
Last ObjectModification:
2015_12_26-PM-09_47_00
Theory : continuity
Home
Index