Nuprl Lemma : bag-max_wf

[A:Type]. ∀[f:A ⟶ ℤ]. ∀[bs:bag(A)].  bag-max(f;bs) ∈ ℤ supposing 0 < #(bs)


Proof




Definitions occuring in Statement :  bag-max: bag-max(f;bs) bag-size: #(bs) bag: bag(T) less_than: a < b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] natural_number: $n int: universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a bag-max: bag-max(f;bs) subtype_rel: A ⊆B nat:
Lemmas referenced :  imax-bag_wf bag-map_wf bag-size-map istype-less_than bag-size_wf bag_wf istype-int istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin closedConclusion intEquality hypothesisEquality hypothesis independent_isectElimination Error :memTop,  axiomEquality equalityTransitivity equalitySymmetry natural_numberEquality applyEquality lambdaEquality_alt setElimination rename inhabitedIsType isect_memberEquality_alt isectIsTypeImplies universeIsType functionIsType instantiate universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[bs:bag(A)].    bag-max(f;bs)  \mmember{}  \mBbbZ{}  supposing  0  <  \#(bs)



Date html generated: 2020_05_20-AM-08_02_09
Last ObjectModification: 2019_12_31-PM-06_32_14

Theory : bags


Home Index