---

Definition: dep-isect
x:A ⋂ B[x] ==  PRIMITIVE

Lemma: dep-isect_wf
∀A:𝕌'. ∀B:A ⟶ 𝕌'.  (x:A ⋂ B[x] ∈ 𝕌')

Lemma: dep-isect-wf
∀A:Type. ∀B:A ⟶ Type.  (x:A ⋂ B[x] ∈ Type)

Lemma: dep-isect-subtype
∀A:Type. ∀B:A ⟶ Type.  (x:A ⋂ B[x] ⊆r A)

Lemma: dep-isect-subtype2
∀[A1,A2:Type]. ∀[B1:A1 ⟶ Type]. ∀[B2:A2 ⟶ Type].
  (x:A1 ⋂ B1[x] ⊆r x:A2 ⋂ B2[x]) supposing ((∀x:A1. (B1[x] ⊆r B2[x])) and (A1 ⊆r A2))

Lemma: member-dep-isect
∀A:Type. ∀B:A ⟶ Type. ∀x:a:A ⋂ B[a].  (x ∈ B[x])

Lemma: strong-continuous-dep-isect
∀A:Type. ∀G:T:Type ⟶ A ⟶ Type.  ((∀a:A. Continuous+(T.G[T;a])) ⇒ Continuous+(T.x:A ⋂ G[T;x]))

Lemma: dep-isect-value-type
∀A:Type. ∀B:A ⟶ Type.  ((value-type(A) ∨ (∀a:A. value-type(B[a]))) ⇒ value-type(a:A ⋂ B[a]))



Home Index