Step
*
of Lemma
fun-connected-tree
∀[T:Type]
∀f:T ⟶ T
∀x,y:T. (x is f*(y)
⇒ (∀z:T. (x is f*(z)
⇒ (z is f*(y) ∨ y is f*(z)))))
supposing ∀a,b:T. (((f a) = (f b) ∈ T)
⇒ (¬((f a) = a ∈ T))
⇒ (¬((f b) = b ∈ T))
⇒ (a = b ∈ T))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN BLemma `fun-connected-induction` THEN Auto) }
1
1. [T] : Type
2. f : T ⟶ T
3. ∀a,b:T. (((f a) = (f b) ∈ T)
⇒ (¬((f a) = a ∈ T))
⇒ (¬((f b) = b ∈ T))
⇒ (a = b ∈ T))
4. x : T
5. y : T
6. z : T
7. x = (f y) ∈ T
8. ¬(x = y ∈ T)
9. y is f*(z)
10. ∀z@0:T. (y is f*(z@0)
⇒ (z@0 is f*(z) ∨ z is f*(z@0)))
11. z@0 : T
12. x is f*(z@0)
⊢ z@0 is f*(z) ∨ z is f*(z@0)
Latex:
Latex:
\mforall{}[T:Type]
\mforall{}f:T {}\mrightarrow{} T
\mforall{}x,y:T. (x is f*(y) {}\mRightarrow{} (\mforall{}z:T. (x is f*(z) {}\mRightarrow{} (z is f*(y) \mvee{} y is f*(z)))))
supposing \mforall{}a,b:T. (((f a) = (f b)) {}\mRightarrow{} (\mneg{}((f a) = a)) {}\mRightarrow{} (\mneg{}((f b) = b)) {}\mRightarrow{} (a = b))
By
Latex:
(RepeatFor 3 ((D 0 THENA Auto)) THEN BLemma `fun-connected-induction` THEN Auto)
Home
Index