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: `b 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: `b supposing a` bag-max: `bag-max(f;bs)` subtype_rel: `A ⊆r 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