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