Nuprl Lemma : fl_all-join

[I:fset(ℕ)]. ∀[i:ℕ]. ∀[a,b:Point(face_lattice(I+i))].  ((∀i.a ∨ b) (∀i.a) ∨ (∀i.b) ∈ Point(face_lattice(I)))


Proof




Definitions occuring in Statement :  fl_all: (∀i.phi) face_lattice: face_lattice(I) add-name: I+i lattice-join: a ∨ b 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 fl_all: (∀i.phi) subtype_rel: A ⊆B guard: {T} bounded-lattice-hom: Hom(l1;l2) and: P ∧ Q so_lambda: λ2x.t[x] implies:  Q prop: names: names(I) nat: bdd-distributive-lattice: BoundedDistributiveLattice so_apply: x[s] uimplies: supposing a lattice-hom: Hom(l1;l2) all: x:A. B[x] true: True squash: T iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  fl-all-hom_wf1 bounded-lattice-hom_wf face_lattice_wf all_wf names_wf not_wf equal_wf lattice-point_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 fl0_wf names-subtype add-name_wf f-subset-add-name fl1_wf trivial-member-add-name1 fset-member_wf nat_wf int-deq_wf strong-subtype-deq-subtype strong-subtype-set3 le_wf strong-subtype-self lattice-0_wf lattice-hom_wf fset_wf squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry applyEquality lambdaEquality setElimination rename setEquality because_Cache sqequalRule productEquality functionEquality intEquality instantiate cumulativity universeEquality independent_isectElimination dependent_functionElimination dependent_set_memberEquality natural_numberEquality lambdaFormation independent_functionElimination isect_memberEquality axiomEquality functionExtensionality imageElimination productElimination imageMemberEquality baseClosed

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].  \mforall{}[a,b:Point(face\_lattice(I+i))].    ((\mforall{}i.a  \mvee{}  b)  =  (\mforall{}i.a)  \mvee{}  (\mforall{}i.b))



Date html generated: 2017_10_05-AM-01_16_21
Last ObjectModification: 2017_07_28-AM-09_32_36

Theory : cubical!type!theory


Home Index