### Nuprl Lemma : sub-isect-family

`∀[P:Type]. ∀[G:P ⟶ Type]. ∀[A:Type]. ∀[F:A ⟶ P ⟶ Type].  G ⊆ ⋂a:A. F[a] supposing ∀a:A. G ⊆ F[a]`

Proof

Definitions occuring in Statement :  sub-family: `F ⊆ G` isect-family: `⋂a:A. F[a]` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` isect-family: `⋂a:A. F[a]` sub-family: `F ⊆ G` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  all_wf sub-family_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaFormation lambdaEquality isect_memberEquality hypothesisEquality applyEquality sqequalHypSubstitution hypothesis dependent_functionElimination thin axiomEquality lemma_by_obid isectElimination because_Cache equalityTransitivity equalitySymmetry functionEquality cumulativity universeEquality

Latex:
\mforall{}[P:Type].  \mforall{}[G:P  {}\mrightarrow{}  Type].  \mforall{}[A:Type].  \mforall{}[F:A  {}\mrightarrow{}  P  {}\mrightarrow{}  Type].    G  \msubseteq{}  \mcap{}a:A.  F[a]  supposing  \mforall{}a:A.  G  \msubseteq{}  F[a]

Date html generated: 2016_05_14-AM-06_12_10
Last ObjectModification: 2015_12_26-PM-00_06_14

Theory : co-recursion

Home Index