Step * of Lemma dM-to-FL-eq-1

[I:fset(ℕ)]. ∀[x:Point(dM(I))].  uiff(dM-to-FL(I;x) 1 ∈ Point(face_lattice(I));x 1 ∈ Point(dM(I)))
BY
Auto }

1
1. fset(ℕ)
2. Point(dM(I))
3. dM-to-FL(I;x) 1 ∈ Point(face_lattice(I))
⊢ 1 ∈ Point(dM(I))

2
1. fset(ℕ)
2. Point(dM(I))
3. 1 ∈ Point(dM(I))
⊢ dM-to-FL(I;x) 1 ∈ Point(face_lattice(I))


Latex:


Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:Point(dM(I))].    uiff(dM-to-FL(I;x)  =  1;x  =  1)


By


Latex:
Auto




Home Index