### Nuprl Lemma : bag-maximals_wf

`∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹].  (bag-maximals(b;R) ∈ bag(T))`

Proof

Definitions occuring in Statement :  bag-maximals: `bag-maximals(bg;R)` bag: `bag(T)` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` bag-maximals: `bag-maximals(bg;R)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` prop: `ℙ` uimplies: `b supposing a`
Lemmas referenced :  bag-filter_wf bag-maximal?_wf subtype_rel_bag assert_wf bool_wf bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality hypothesis applyEquality setEquality independent_isectElimination setElimination rename because_Cache axiomEquality equalityTransitivity equalitySymmetry functionEquality isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].    (bag-maximals(b;R)  \mmember{}  bag(T))

Date html generated: 2016_05_15-PM-02_30_41
Last ObjectModification: 2015_12_27-AM-09_48_37

Theory : bags

Home Index