Step
*
1
of Lemma
f-subset-singleton
1. [A] : Type
2. [eq] : EqDecider(A)
3. [a] : A
4. x : fset(A)
5. ∀a@0:A. a@0 = a ∈ A supposing a@0 ∈ x
⊢ (x = {a} ∈ fset(A)) ∨ (x = {} ∈ fset(A))
BY
{ (Decide ↑fset-null(x) THENA Auto) }
1
1. [A] : Type
2. [eq] : EqDecider(A)
3. [a] : A
4. x : fset(A)
5. ∀a@0:A. a@0 = a ∈ A supposing a@0 ∈ x
6. ↑fset-null(x)
⊢ (x = {a} ∈ fset(A)) ∨ (x = {} ∈ fset(A))
2
1. [A] : Type
2. [eq] : EqDecider(A)
3. [a] : A
4. x : fset(A)
5. ∀a@0:A. a@0 = a ∈ A supposing a@0 ∈ x
6. ¬↑fset-null(x)
⊢ (x = {a} ∈ fset(A)) ∨ (x = {} ∈ fset(A))
Latex:
Latex:
1. [A] : Type
2. [eq] : EqDecider(A)
3. [a] : A
4. x : fset(A)
5. \mforall{}a@0:A. a@0 = a supposing a@0 \mmember{} x
\mvdash{} (x = \{a\}) \mvee{} (x = \{\})
By
Latex:
(Decide \muparrow{}fset-null(x) THENA Auto)
Home
Index