Step
*
1
1
of Lemma
constrained-antichain-lattice_wf
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. ∀x,y:fset(T). (y ⊆ x
⇒ (↑(P x))
⇒ (↑(P y)))
5. ↑(P {})
6. {{}} ∈ fset(fset(T))
7. ↑fset-antichain(eq;{{}})
8. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))]. uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
9. x : fset(T)
10. x = {} ∈ fset(T)
⊢ ↑(P x)
BY
{ (HypSubst' (-1) 0 THEN Auto) }
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) {}\mrightarrow{} \mBbbB{}
4. \mforall{}x,y:fset(T). (y \msubseteq{} x {}\mRightarrow{} (\muparrow{}(P x)) {}\mRightarrow{} (\muparrow{}(P y)))
5. \muparrow{}(P \{\})
6. \{\{\}\} \mmember{} fset(fset(T))
7. \muparrow{}fset-antichain(eq;\{\{\}\})
8. \mforall{}[P:fset(T) {}\mrightarrow{} \mBbbB{}]. \mforall{}[s:fset(fset(T))].
uiff(fset-all(s;x.P[x]);\mforall{}[x:fset(T)]. \muparrow{}P[x] supposing x \mmember{} s)
9. x : fset(T)
10. x = \{\}
\mvdash{} \muparrow{}(P x)
By
Latex:
(HypSubst' (-1) 0 THEN Auto)
Home
Index