Step
*
2
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. ¬¬(∃c:fset(T). (c ∈ Cs[x] ∧ c ⊆ {x}))
10. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))]. uiff({x ∈ s | P[x]} = {} ∈ fset(fset(T));¬(∃x:fset(T). (x ∈ s ∧ (↑P[x]))))
⊢ 0 = (f x) ∈ Point(L)
BY
{ ((Assert ∀x,y:Point(L). Dec(x = y ∈ Point(L)) BY Auto) THEN SupposeNot THEN D -4 THEN (D 0 THENA Auto)) }
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). (c ∈ Cs[x] ∧ 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. \mneg{}\mneg{}(\mexists{}c:fset(T). (c \mmember{} Cs[x] \mwedge{} c \msubseteq{} \{x\}))
10. \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]))))
\mvdash{} 0 = (f x)
By
Latex:
((Assert \mforall{}x,y:Point(L). Dec(x = y) BY Auto) THEN SupposeNot THEN D -4 THEN (D 0 THENA Auto))
Home
Index