Step * of Lemma fl-morph-fset-join

No Annotations
[A,B:fset(ℕ)]. ∀[g:A ⟶ B]. ∀[x:fset(Point(face_lattice(B)))].  ((\/(x))<g> \/(<g>"(x)) ∈ Point(face_lattice(A)))
BY
Auto }


Latex:


Latex:
No  Annotations
\mforall{}[A,B:fset(\mBbbN{})].  \mforall{}[g:A  {}\mrightarrow{}  B].  \mforall{}[x:fset(Point(face\_lattice(B)))].    ((\mbackslash{}/(x))<g>  =  \mbackslash{}/(<g>"(x)))


By


Latex:
Auto




Home Index