---

Step * of Lemma stable-union-metric-subspace

∀[X:Type]. ∀[d:metric(X)]. ∀[T:Type]. ∀[P:T ⟶ X ⟶ ℙ].
  metric-subspace(X;d;stable-union(X;T;i,x.P[i;x])) supposing ∀i:T. ∀x,y:X.  (P[i;x] ⇒ y ≡ x ⇒ P[i;y])
BY
{ (Auto THEN (D 0 THENL [Auto; ((D 0 THENA Auto) THEN D -1 THEN Auto)])) }

1
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])

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}].
    metric-subspace(X;d;stable-union(X;T;i,x.P[i;x])) 
    supposing  \mforall{}i:T.  \mforall{}x,y:X.    (P[i;x]  {}\mRightarrow{}  y  \mequiv{}  x  {}\mRightarrow{}  P[i;y])


By

---

Latex:
(Auto  THEN  (D  0  THENL  [Auto;  ((D  0  THENA  Auto)  THEN  D  -1  THEN  Auto)]))

---

Home Index