---

Step * 1 1 of Lemma face-lattice-0-not-1


1. J : fset(ℕ)
2. {} = {{}} ∈ Point(face_lattice(J))
⊢ False
BY
{ (Unfold `face_lattice` -1
   THEN (Assert ⌜{}
                 = {{}}
                 ∈ {ac:fset(fset(names(J) + names(J)))| 
                    (↑fset-antichain(union-deq(names(J);names(J);NamesDeq;NamesDeq);ac))
                    ∧ (∀a:fset(names(J) + names(J)). (a ∈ ac ⇒ (∀z:names(J). (¬(inl z ∈ a ∧ inr z  ∈ a)))))} ⌝⋅
         THENA (SubsumeC ⌜Point(face-lattice(names(J);NamesDeq))⌝⋅
                THEN Auto
                THEN InstLemma `fl-point` [⌜names(J)⌝;⌜NamesDeq⌝]⋅
                THEN Auto)
         )
   THEN (EqTypeHD (-1) THENA Auto)
   THEN Thin (-1)) }

1
1. J : fset(ℕ)
2. {} = {{}} ∈ Point(face-lattice(names(J);NamesDeq))
3. {} = {{}} ∈ fset(fset(names(J) + names(J)))
⊢ False

---

Latex:

---

Latex:

1.  J  :  fset(\mBbbN{})
2.  \{\}  =  \{\{\}\}
\mvdash{}  False


By

---

Latex:
(Unfold  `face\_lattice`  -1
  THEN  (Assert  \mkleeneopen{}\{\}  =  \{\{\}\}\mkleeneclose{}\mcdot{}
              THENA  (SubsumeC  \mkleeneopen{}Point(face-lattice(names(J);NamesDeq))\mkleeneclose{}\mcdot{}
                            THEN  Auto
                            THEN  InstLemma  `fl-point`  [\mkleeneopen{}names(J)\mkleeneclose{};\mkleeneopen{}NamesDeq\mkleeneclose{}]\mcdot{}
                            THEN  Auto)
              )
  THEN  (EqTypeHD  (-1)  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index