Nuprl Lemma : dM1_wf

[I:fset(ℕ)]. (1 ∈ Point(dM(I)))


Proof




Definitions occuring in Statement :  dM1: 1 dM: dM(I) lattice-point: Point(l) fset: fset(T) nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T dM1: 1 subtype_rel: A ⊆B DeMorgan-algebra: DeMorganAlgebra so_lambda: λ2x.t[x] prop: and: P ∧ Q guard: {T} uimplies: supposing a so_apply: x[s]
Lemmas referenced :  lattice-1_wf dM_wf subtype_rel_set DeMorgan-algebra-structure_wf bounded-lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype DeMorgan-algebra-structure-subtype subtype_rel_transitivity lattice-structure_wf bounded-lattice-axioms_wf uall_wf lattice-point_wf equal_wf lattice-meet_wf lattice-join_wf DeMorgan-algebra-axioms_wf fset_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality instantiate lambdaEquality productEquality independent_isectElimination cumulativity universeEquality because_Cache axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[I:fset(\mBbbN{})].  (1  \mmember{}  Point(dM(I)))



Date html generated: 2016_05_18-AM-11_56_50
Last ObjectModification: 2015_12_28-PM-03_08_50

Theory : cubical!type!theory


Home Index