Nuprl Lemma : ball_cons_lemma

f,as,a,T:Top.  (∀bx(:T) ∈ [a as]. f[x] f[a] ∧b (∀bx(:T) ∈ as. f[x]))


Proof




Definitions occuring in Statement :  ball: ball cons: [a b] band: p ∧b q top: Top so_apply: x[s] all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T ball: ball so_lambda: λ2x.t[x] top: Top so_apply: x[s] band_mon: <𝔹,∧b> grp_op: * pi2: snd(t) pi1: fst(t) infix_ap: y
Lemmas referenced :  top_wf mon_for_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}f,as,a,T:Top.    (\mforall{}\msubb{}x(:T)  \mmember{}  [a  /  as].  f[x]  \msim{}  f[a]  \mwedge{}\msubb{}  (\mforall{}\msubb{}x(:T)  \mmember{}  as.  f[x]))



Date html generated: 2016_05_16-AM-07_37_13
Last ObjectModification: 2015_12_28-PM-05_45_15

Theory : list_2


Home Index