Nuprl Lemma : equal-Sierpinski-bottom

[x:ℕ ⟶ 𝔹]. uiff(x = ⊥ ∈ (ℕ ⟶ 𝔹);∀n:ℕ(¬↑(x n)))


Proof




Definitions occuring in Statement :  Sierpinski-bottom: nat: assert: b bool: 𝔹 uiff: uiff(P;Q) uall: [x:A]. B[x] all: x:A. B[x] not: ¬A apply: a function: x:A ⟶ B[x] equal: t ∈ T
Definitions unfolded in proof :  Sierpinski-bottom: uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a all: x:A. B[x] not: ¬A implies:  Q false: False assert: b ifthenelse: if then else fi  bfalse: ff prop: subtype_rel: A ⊆B top: Top guard: {T} iff: ⇐⇒ Q rev_implies:  Q so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  assert_wf bfalse_wf top_wf nat_wf assert_functionality_wrt_uiff not_wf equal_wf bool_wf iff_imp_equal_bool false_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lambdaFormation thin sqequalHypSubstitution hypothesis lemma_by_obid isectElimination applyEquality lambdaEquality hypothesisEquality isect_memberEquality voidElimination voidEquality sqequalRule addLevel impliesFunctionality because_Cache independent_isectElimination productElimination independent_functionElimination dependent_functionElimination functionEquality functionExtensionality independent_pairEquality equalityTransitivity equalitySymmetry axiomEquality

Latex:
\mforall{}[x:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  uiff(x  =  \mbot{};\mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}(x  n)))



Date html generated: 2019_10_31-AM-06_35_16
Last ObjectModification: 2015_12_28-AM-11_21_54

Theory : synthetic!topology


Home Index