### Nuprl Lemma : bounded-ccc-nset-finite

K:Type. (CCCNSet(K)  (∀B:ℕ((∀k:K. (k ≤ B))  finite(K))))

Proof

Definitions occuring in Statement :  ccc-nset: CCCNSet(K) finite: finite(T) nat: le: A ≤ B all: x:A. B[x] implies:  Q universe: Type
Definitions unfolded in proof :  prop: uimplies: supposing a nat: guard: {T} subtype_rel: A ⊆B uall: [x:A]. B[x] and: P ∧ Q ccc-nset: CCCNSet(K) implies:  Q member: t ∈ T all: x:A. B[x]
Lemmas referenced :  istype-universe ccc-nset_wf istype-nat nat_wf subtype_rel_transitivity istype-le bounded-decidable-nset-finite bounded-ccc-nset-decidable
Rules used in proof :  universeEquality instantiate independent_isectElimination intEquality Error :inhabitedIsType,  rename setElimination Error :lambdaEquality_alt,  applyEquality isectElimination Error :universeIsType,  Error :functionIsType,  sqequalRule productElimination independent_functionElimination hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution hypothesis Error :lambdaFormation_alt,  sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution extract_by_obid introduction cut

Latex:
\mforall{}K:Type.  (CCCNSet(K)  {}\mRightarrow{}  (\mforall{}B:\mBbbN{}.  ((\mforall{}k:K.  (k  \mleq{}  B))  {}\mRightarrow{}  finite(K))))

Date html generated: 2019_06_20-PM-03_02_40
Last ObjectModification: 2019_06_13-PM-04_17_15

Theory : continuity

Home Index