Nuprl Lemma : Sierpinski-unequal-1

⊥ = ⊤ ∈ (ℕ ⟶ 𝔹⇐⇒ False


Proof




Definitions occuring in Statement :  Sierpinski-top: Sierpinski-bottom: nat: bool: 𝔹 iff: ⇐⇒ Q false: False function: x:A ⟶ B[x] equal: t ∈ T
Definitions unfolded in proof :  iff: ⇐⇒ Q and: P ∧ Q implies:  Q false: False member: t ∈ T all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uall: [x:A]. B[x] uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top prop: nat: le: A ≤ B less_than': less_than'(a;b) not: ¬A Sierpinski-top: Sierpinski-bottom: rev_implies:  Q
Lemmas referenced :  Sierpinski-top_wf Sierpinski-bottom_wf bool_wf nat_wf equal_wf btrue_neq_bfalse le_wf false_wf int_formula_prop_wf int_term_value_constant_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermConstant_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt decidable__equal_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation lambdaFormation cut applyEquality lambdaEquality hypothesisEquality lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin natural_numberEquality because_Cache hypothesis unionElimination isectElimination independent_isectElimination dependent_pairFormation intEquality isect_memberEquality voidElimination voidEquality sqequalRule computeAll dependent_set_memberEquality equalityTransitivity equalitySymmetry equalityUniverse levelHypothesis independent_functionElimination functionEquality

Latex:
\mbot{}  =  \mtop{}  \mLeftarrow{}{}\mRightarrow{}  False



Date html generated: 2019_10_31-AM-06_35_21
Last ObjectModification: 2016_01_17-AM-09_35_56

Theory : synthetic!topology


Home Index