Step
*
of Lemma
qle_connex
∀a,b:ℚ. ((a ≤ b) ∨ (b ≤ a))
BY
{ ((UnivCD THENA Auto) THEN (InstLemma `qless_trichot_qorder` [⌜a⌝;⌜b⌝]⋅ THENA Auto) THEN ParallelLast) }
1
1. a : ℚ@i
2. b : ℚ@i
3. a < b
⊢ a ≤ b
2
1. a : ℚ@i
2. b : ℚ@i
3. (a = b ∈ ℚ) ∨ b < a
⊢ b ≤ a
Latex:
Latex:
\mforall{}a,b:\mBbbQ{}. ((a \mleq{} b) \mvee{} (b \mleq{} a))
By
Latex:
((UnivCD THENA Auto)
THEN (InstLemma `qless\_trichot\_qorder` [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{} THENA Auto)
THEN ParallelLast)
Home
Index