Step
*
1
1
1
of Lemma
equipollent-split
1. [T] : Type
2. [P] : T ⟶ ℙ
3. p : x:T ⟶ (↓P[x] + (¬↓P[x]))
⊢ Bij(T;{x:T| ↓P[x]} + {x:T| ↓¬P[x]} ;λx.case p x of inl(z) => inl x | inr(z) => inr x )
BY
{ ((RepeatFor 2 (D 0) THEN Reduce 0) THENA Auto) }
1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. p : x:T ⟶ (↓P[x] + (¬↓P[x]))
4. a1 : T
⊢ ∀a2:T
((case p a1 of inl(z) => inl a1 | inr(z) => inr a1
= case p a2 of inl(z) => inl a2 | inr(z) => inr a2
∈ ({x:T| ↓P[x]} + {x:T| ↓¬P[x]} ))
⇒ (a1 = a2 ∈ T))
2
1. [T] : Type
2. [P] : T ⟶ ℙ
3. p : x:T ⟶ (↓P[x] + (¬↓P[x]))
4. b : {x:T| ↓P[x]} + {x:T| ↓¬P[x]}
⊢ ∃a:T. (case p a of inl(z) => inl a | inr(z) => inr a = b ∈ ({x:T| ↓P[x]} + {x:T| ↓¬P[x]} ))
Latex:
Latex:
1. [T] : Type
2. [P] : T {}\mrightarrow{} \mBbbP{}
3. p : x:T {}\mrightarrow{} (\mdownarrow{}P[x] + (\mneg{}\mdownarrow{}P[x]))
\mvdash{} Bij(T;\{x:T| \mdownarrow{}P[x]\} + \{x:T| \mdownarrow{}\mneg{}P[x]\} ;\mlambda{}x.case p x of inl(z) => inl x | inr(z) => inr x )
By
Latex:
((RepeatFor 2 (D 0) THEN Reduce 0) THENA Auto)
Home
Index