Nuprl Lemma : neg-dM_inc

[I:fset(ℕ)]. ∀[x:names(I)].  (<x>= <1-x> ∈ Point(dM(I)))


Proof




Definitions occuring in Statement :  dM_opp: <1-x> dM_inc: <x> dM: dM(I) names-deq: NamesDeq names: names(I) dm-neg: ¬(x) lattice-point: Point(l) fset: fset(T) nat: uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T dM_opp: <1-x> dM_inc: <x> dM: dM(I) top: Top squash: T prop: subtype_rel: A ⊆B bdd-distributive-lattice: BoundedDistributiveLattice so_lambda: λ2x.t[x] and: P ∧ Q so_apply: x[s] uimplies: supposing a true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  free-dma-point equal_wf squash_wf true_wf lattice-point_wf free-DeMorgan-lattice_wf names_wf names-deq_wf subtype_rel_set bounded-lattice-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype bounded-lattice-axioms_wf uall_wf lattice-meet_wf lattice-join_wf dm-neg-inc dmopp_wf iff_weakening_equal fset_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesis applyEquality lambdaEquality imageElimination hypothesisEquality equalityTransitivity equalitySymmetry universeEquality because_Cache instantiate productEquality cumulativity independent_isectElimination natural_numberEquality imageMemberEquality baseClosed productElimination independent_functionElimination axiomEquality

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:names(I)].    (\mneg{}(<x>)  =  ə-x>)



Date html generated: 2017_10_05-AM-00_59_33
Last ObjectModification: 2017_07_28-AM-09_25_21

Theory : cubical!type!theory


Home Index