---

Step * of Lemma member-approx-type

∀[T:Type]. ∀x:Base. uiff(x ∈ approx-type(T);↓∃t:Base. ((x ≤ t) ∧ (t ∈ T)))
BY
{ Auto }

1
1. T : Type
2. x : Base
3. x ∈ approx-type(T)
⊢ ↓∃t:Base. ((x ≤ t) ∧ (t ∈ T))

2
1. T : Type
2. x : Base
3. ∃t:Base. ((x ≤ t) ∧ (t ∈ T))
⊢ x ∈ approx-type(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:Base.  uiff(x  \mmember{}  approx-type(T);\mdownarrow{}\mexists{}t:Base.  ((x  \mleq{}  t)  \mwedge{}  (t  \mmember{}  T)))


By

---

Latex:
Auto

---

Home Index