---

Step * 1 of Lemma stable-union-metric-subspace


1. X : Type
2. d : metric(X)
3. T : Type
4. P : T ⟶ X ⟶ ℙ
5. ∀i:T. ∀x,y:X.  (P[i;x] ⇒ y ≡ x ⇒ P[i;y])
6. a : X
7. ¬¬(∃i:T. P[i;a])
8. x : X
9. x ≡ a
⊢ x ∈ stable-union(X;T;i,x.P[i;x])
BY
{ (MemTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  T  :  Type
4.  P  :  T  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}i:T.  \mforall{}x,y:X.    (P[i;x]  {}\mRightarrow{}  y  \mequiv{}  x  {}\mRightarrow{}  P[i;y])
6.  a  :  X
7.  \mneg{}\mneg{}(\mexists{}i:T.  P[i;a])
8.  x  :  X
9.  x  \mequiv{}  a
\mvdash{}  x  \mmember{}  stable-union(X;T;i,x.P[i;x])


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index