Step
*
1
1
2
2
1
1
1
of Lemma
fl-all-decomp
1. T : Type
2. eq : EqDecider(T)
3. phi : Point(face-lattice(T;eq))
4. i : T
5. ∀x,y:Point(face-lattice(T;eq)). (x ≤ y
⇒ y ≤ x
⇒ (x = y ∈ Point(face-lattice(T;eq))))
6. Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))
7. s : fset(T + T)
8. s ∈ phi
9. ¬inl i ∈ s
10. ¬inr i ∈ s
⊢ s ∈ {x ∈ phi | (¬binl i ∈b x) ∧b (¬binr i ∈b x)}
BY
{ (BLemma `member-fset-filter` THEN Auto) }
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. phi : Point(face-lattice(T;eq))
4. i : T
5. \mforall{}x,y:Point(face-lattice(T;eq)). (x \mleq{} y {}\mRightarrow{} y \mleq{} x {}\mRightarrow{} (x = y))
6. Point(face-lattice(T;eq)) \msubseteq{}r fset(fset(T + T))
7. s : fset(T + T)
8. s \mmember{} phi
9. \mneg{}inl i \mmember{} s
10. \mneg{}inr i \mmember{} s
\mvdash{} s \mmember{} \{x \mmember{} phi | (\mneg{}\msubb{}inl i \mmember{}\msubb{} x) \mwedge{}\msubb{} (\mneg{}\msubb{}inr i \mmember{}\msubb{} x)\}
By
Latex:
(BLemma `member-fset-filter` THEN Auto)
Home
Index