Step
*
2
1
1
1
of Lemma
lattice-extend-dlwc-inc
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. L : BoundedDistributiveLattice
5. eqL : EqDecider(Point(L))
6. f : T ⟶ Point(L)
7. ∀x:T. ∀c:fset(T). (c ∈ Cs[x]
⇒ (/\(f"(c)) = 0 ∈ Point(L)))
8. x : T
9. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))]. uiff({x ∈ s | P[x]} = {} ∈ fset(fset(T));¬(∃x:fset(T). (x ∈ s ∧ (↑P[x]))))
10. ∀x,y:Point(L). Dec(x = y ∈ Point(L))
11. ¬(0 = (f x) ∈ Point(L))
12. ∃c:fset(T). (c ∈ Cs[x] ∧ c ⊆ {x})
⊢ False
BY
{ ExRepD }
1
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. L : BoundedDistributiveLattice
5. eqL : EqDecider(Point(L))
6. f : T ⟶ Point(L)
7. ∀x:T. ∀c:fset(T). (c ∈ Cs[x]
⇒ (/\(f"(c)) = 0 ∈ Point(L)))
8. x : T
9. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))]. uiff({x ∈ s | P[x]} = {} ∈ fset(fset(T));¬(∃x:fset(T). (x ∈ s ∧ (↑P[x]))))
10. ∀x,y:Point(L). Dec(x = y ∈ Point(L))
11. ¬(0 = (f x) ∈ Point(L))
12. c : fset(T)@i
13. c ∈ Cs[x]
14. c ⊆ {x}
⊢ False
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. Cs : T {}\mrightarrow{} fset(fset(T))
4. L : BoundedDistributiveLattice
5. eqL : EqDecider(Point(L))
6. f : T {}\mrightarrow{} Point(L)
7. \mforall{}x:T. \mforall{}c:fset(T). (c \mmember{} Cs[x] {}\mRightarrow{} (/\mbackslash{}(f"(c)) = 0))
8. x : T
9. \mforall{}[P:fset(T) {}\mrightarrow{} \mBbbB{}]. \mforall{}[s:fset(fset(T))].
uiff(\{x \mmember{} s | P[x]\} = \{\};\mneg{}(\mexists{}x:fset(T). (x \mmember{} s \mwedge{} (\muparrow{}P[x]))))
10. \mforall{}x,y:Point(L). Dec(x = y)
11. \mneg{}(0 = (f x))
12. \mexists{}c:fset(T). (c \mmember{} Cs[x] \mwedge{} c \msubseteq{} \{x\})
\mvdash{} False
By
Latex:
ExRepD
Home
Index