Step
*
of Lemma
fl0-not-1
∀[I:fset(ℕ)]. ∀[x:names(I)]. (¬((x=0) = 1 ∈ Point(face_lattice(I))))
BY
{ (Auto
THEN (D 0 THENA Auto)
THEN RepUR ``fl0 face-lattice0 lattice-1 face_lattice face-lattice`` -1
THEN RepUR ``lattice-point free-dist-lattice-with-constraints`` -1
THEN RepUR ``constrained-antichain-lattice mk-bounded-distributive-lattice`` -1
THEN RepUR ``mk-bounded-lattice`` -1
THEN (EqTypeHD (-1) THENA Auto)
THEN Thin (-1)) }
1
1. I : fset(ℕ)
2. x : names(I)
3. {{inl x}} = {{}} ∈ fset(fset(names(I) + names(I)))
⊢ False
Latex:
Latex:
\mforall{}[I:fset(\mBbbN{})]. \mforall{}[x:names(I)]. (\mneg{}((x=0) = 1))
By
Latex:
(Auto
THEN (D 0 THENA Auto)
THEN RepUR ``fl0 face-lattice0 lattice-1 face\_lattice face-lattice`` -1
THEN RepUR ``lattice-point free-dist-lattice-with-constraints`` -1
THEN RepUR ``constrained-antichain-lattice mk-bounded-distributive-lattice`` -1
THEN RepUR ``mk-bounded-lattice`` -1
THEN (EqTypeHD (-1) THENA Auto)
THEN Thin (-1))
Home
Index