Nuprl Lemma : lattice-hom-fset-meet

[l1,l2:BoundedLattice]. ∀[eq1:EqDecider(Point(l1))]. ∀[eq2:EqDecider(Point(l2))]. ∀[f:Hom(l1;l2)].
[s:fset(Point(l1))].
  ((f /\(s)) /\(f"(s)) ∈ Point(l2))


Proof




Definitions occuring in Statement :  lattice-fset-meet: /\(s) bounded-lattice-hom: Hom(l1;l2) bdd-lattice: BoundedLattice lattice-point: Point(l) fset-image: f"(s) fset: fset(T) deq: EqDecider(T) uall: [x:A]. B[x] apply: a equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T fset: fset(T) subtype_rel: A ⊆B quotient: x,y:A//B[x; y] and: P ∧ Q bdd-lattice: BoundedLattice so_lambda: λ2x.t[x] prop: so_apply: x[s] uimplies: supposing a all: x:A. B[x] implies:  Q nat: false: False ge: i ≥  not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top or: P ∨ Q cons: [a b] decidable: Dec(P) colength: colength(L) nil: [] it: guard: {T} sq_type: SQType(T) less_than: a < b squash: T less_than': less_than'(a;b) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] empty-fset: {} lattice-fset-meet: /\(s) bounded-lattice-hom: Hom(l1;l2) lattice-hom: Hom(l1;l2) true: True iff: ⇐⇒ Q rev_implies:  Q fset-add: fset-add(eq;x;s) fset-union: x ⋃ y l-union: as ⋃ bs reduce: reduce(f;k;as) list_ind: list_ind
Lemmas referenced :  lattice-point_wf list_wf set-equal_wf subtype_rel_set bounded-lattice-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype bounded-lattice-axioms_wf fset_wf bounded-lattice-hom_wf deq_wf bdd-lattice_wf nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than list-cases product_subtype_list colength-cons-not-zero colength_wf_list decidable__le intformnot_wf int_formula_prop_not_lemma istype-le subtract-1-ge-0 subtype_base_sq intformeq_wf int_formula_prop_eq_lemma set_subtype_base int_subtype_base spread_cons_lemma decidable__equal_int subtract_wf itermSubtract_wf itermAdd_wf int_term_value_subtract_lemma int_term_value_add_lemma le_wf istype-nat fset-image-empty reduce_nil_lemma reduce_cons_lemma equal_wf squash_wf true_wf istype-universe lattice-hom-meet lattice-fset-meet_wf decidable-equal-deq list_subtype_fset lattice-meet_wf subtype_rel_self iff_weakening_equal fset-image_wf fset-add-as-cons fset-union_wf fset-singleton_wf decidable_wf fset-image-union lattice-fset-meet-union fset-image-singleton lattice-fset-meet-singleton quotient-member-eq set-equal-equiv
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality extract_by_obid isectElimination thin hypothesisEquality applyEquality because_Cache hypothesis sqequalRule pertypeElimination promote_hyp productElimination productIsType equalityIstype universeIsType sqequalBase equalitySymmetry instantiate lambdaEquality_alt productEquality cumulativity independent_isectElimination isect_memberEquality_alt axiomEquality isectIsTypeImplies inhabitedIsType setElimination rename independent_pairFormation equalityTransitivity lambdaFormation_alt dependent_functionElimination independent_functionElimination intWeakElimination natural_numberEquality approximateComputation dependent_pairFormation_alt int_eqEquality voidElimination functionIsTypeImplies unionElimination hypothesis_subsumption dependent_set_memberEquality_alt applyLambdaEquality imageElimination baseApply closedConclusion baseClosed intEquality voidEquality isect_memberEquality universeEquality imageMemberEquality hyp_replacement functionEquality functionIsType

Latex:
\mforall{}[l1,l2:BoundedLattice].  \mforall{}[eq1:EqDecider(Point(l1))].  \mforall{}[eq2:EqDecider(Point(l2))].  \mforall{}[f:Hom(l1;l2)].
\mforall{}[s:fset(Point(l1))].
    ((f  /\mbackslash{}(s))  =  /\mbackslash{}(f"(s)))



Date html generated: 2020_05_20-AM-08_44_48
Last ObjectModification: 2018_12_13-PM-02_29_51

Theory : lattices


Home Index