Step
*
1
1
1
1
1
1
of Lemma
fset-ac-le-face-lattice0
.....assertion.....
1. T : Type
2. eq : EqDecider(T)
3. i : T
4. s : fset(fset(T + T))
5. Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))
6. ∀[x:fset(T + T)]. ↑inl i ∈b x supposing x ∈ s
7. x : fset(T + T)
8. x ∈ s
9. ↑inl i ∈b x
10. {y ∈ (i=0) | deq-f-subset(union-deq(T;T;eq;eq)) y x} = {} ∈ fset(fset(T + T))
⊢ {inl i} ∈ {y ∈ (i=0) | deq-f-subset(union-deq(T;T;eq;eq)) y x}
BY
{ (Thin (-1) THEN MoveToConcl (-1) THEN Unfold `face-lattice0` 0 THEN (GenConcl ⌜(inl i) = a ∈ (T + T)⌝⋅ THENA Auto)) }
1
1. T : Type
2. eq : EqDecider(T)
3. i : T
4. s : fset(fset(T + T))
5. Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))
6. ∀[x:fset(T + T)]. ↑inl i ∈b x supposing x ∈ s
7. x : fset(T + T)
8. x ∈ s
9. a : T + T
10. (inl i) = a ∈ (T + T)
⊢ (↑a ∈b x)
⇒ {a} ∈ {y ∈ {{a}} | deq-f-subset(union-deq(T;T;eq;eq)) y x}
Latex:
Latex:
.....assertion.....
1. T : Type
2. eq : EqDecider(T)
3. i : T
4. s : fset(fset(T + T))
5. Point(face-lattice(T;eq)) \msubseteq{}r fset(fset(T + T))
6. \mforall{}[x:fset(T + T)]. \muparrow{}inl i \mmember{}\msubb{} x supposing x \mmember{} s
7. x : fset(T + T)
8. x \mmember{} s
9. \muparrow{}inl i \mmember{}\msubb{} x
10. \{y \mmember{} (i=0) | deq-f-subset(union-deq(T;T;eq;eq)) y x\} = \{\}
\mvdash{} \{inl i\} \mmember{} \{y \mmember{} (i=0) | deq-f-subset(union-deq(T;T;eq;eq)) y x\}
By
Latex:
(Thin (-1)
THEN MoveToConcl (-1)
THEN Unfold `face-lattice0` 0
THEN (GenConcl \mkleeneopen{}(inl i) = a\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index