Step
*
1
of Lemma
fset-only_wf
1. T : Type
2. eq : EqDecider(T)
3. P : T ⟶ 𝔹
4. s : fset(T)
5. ¬(∀x:T. (x ∈ s
⇒ (¬↑P[x])))
6. ∀x,y:T. (x ∈ s
⇒ y ∈ s
⇒ (↑P[x])
⇒ (↑P[y])
⇒ (x = y ∈ T))
⊢ only x ∈ s s.t. P[x] ∈ {x:T| x ∈ s ∧ (↑P[x])}
BY
{ Unfold `fset-only` 0 }
1
1. T : Type
2. eq : EqDecider(T)
3. P : T ⟶ 𝔹
4. s : fset(T)
5. ¬(∀x:T. (x ∈ s
⇒ (¬↑P[x])))
6. ∀x,y:T. (x ∈ s
⇒ y ∈ s
⇒ (↑P[x])
⇒ (↑P[y])
⇒ (x = y ∈ T))
⊢ item({x ∈ s | P[x]}) ∈ {x:T| x ∈ s ∧ (↑P[x])}
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. P : T {}\mrightarrow{} \mBbbB{}
4. s : fset(T)
5. \mneg{}(\mforall{}x:T. (x \mmember{} s {}\mRightarrow{} (\mneg{}\muparrow{}P[x])))
6. \mforall{}x,y:T. (x \mmember{} s {}\mRightarrow{} y \mmember{} s {}\mRightarrow{} (\muparrow{}P[x]) {}\mRightarrow{} (\muparrow{}P[y]) {}\mRightarrow{} (x = y))
\mvdash{} only x \mmember{} s s.t. P[x] \mmember{} \{x:T| x \mmember{} s \mwedge{} (\muparrow{}P[x])\}
By
Latex:
Unfold `fset-only` 0
Home
Index