---

Step * of Lemma name-morph-satisfies-fset-join

∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀s:fset(Point(face_lattice(I))).
  ((\/(s) f) = 1 ⇐⇒ ↓∃a:Point(face_lattice(I)). (a ∈ s ∧ (a f) = 1))
BY
{ (RepeatFor 3 (Intro) THEN (Using [`eq',⌜face_lattice-deq()⌝] (BLemma `fset-induction`)⋅ THENA Auto)) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : J ⟶ I
⊢ ∀s:fset(Point(face_lattice(I))). SqStable((\/(s) f) = 1 ⇐⇒ ↓∃a:Point(face_lattice(I)). (a ∈ s ∧ (a f) = 1))

2
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : J ⟶ I
⊢ (\/({}) f) = 1 ⇐⇒ ↓∃a:Point(face_lattice(I)). (a ∈ {} ∧ (a f) = 1)

3
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : J ⟶ I
⊢ ∀s:fset(Point(face_lattice(I))). ∀x:Point(face_lattice(I)).
    (((\/(s) f) = 1 ⇐⇒ ↓∃a:Point(face_lattice(I)). (a ∈ s ∧ (a f) = 1))
    ⇒ (\/(fset-add(face_lattice-deq();x;s)) f) = 1
       ⇐⇒ ↓∃a:Point(face_lattice(I)). (a ∈ fset-add(face_lattice-deq();x;s) ∧ (a f) = 1) 
       supposing ¬x ∈ s)

---

Latex:

---

Latex:
\mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}s:fset(Point(face\_lattice(I))).
    ((\mbackslash{}/(s)  f)  =  1  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}a:Point(face\_lattice(I)).  (a  \mmember{}  s  \mwedge{}  (a  f)  =  1))


By

---

Latex:
(RepeatFor  3  (Intro)  THEN  (Using  [`eq',\mkleeneopen{}face\_lattice-deq()\mkleeneclose{}]  (BLemma  `fset-induction`)\mcdot{}  THENA  Auto))

---

Home Index