---

Step * of Lemma global-class-iff-bounded-local-class

∀[Info:Type]. ∀[A:{A:Type| valueall-type(A)} ]. ∀[X:EClass(A)].
  (GlobalClass(Info;A;X) ⇐⇒ LocalClass(X) ∧ LocBounded(A;X))
BY
{ Auto }

1
1. [Info] : Type
2. [A] : {A:Type| valueall-type(A)} 
3. [X] : EClass(A)
4. GlobalClass(Info;A;X)@i'
⊢ LocalClass(X)

2
1. [Info] : Type
2. [A] : {A:Type| valueall-type(A)} 
3. [X] : EClass(A)
4. GlobalClass(Info;A;X)@i'
⊢ LocBounded(A;X)

3
1. [Info] : Type
2. [A] : {A:Type| valueall-type(A)} 
3. [X] : EClass(A)
4. LocalClass(X)@i'
5. LocBounded(A;X)@i'
⊢ GlobalClass(Info;A;X)

---

Latex:


\mforall{}[Info:Type].  \mforall{}[A:\{A:Type|  valueall-type(A)\}  ].  \mforall{}[X:EClass(A)].
    (GlobalClass(Info;A;X)  \mLeftarrow{}{}\mRightarrow{}  LocalClass(X)  \mwedge{}  LocBounded(A;X))


By

Auto

---

Home Index