Actions: UniMath/agda-unimath
Actions
291 workflow runs
291 workflow runs
x y : ℚ
, x < y
if and only if real-ℚ x < real-ℚ y
(#1293)
Build and deploy library website
#661:
Commit c0178ea
pushed
by
fredrik-bakke
x y : ℚ
, x ≤ y
if and only if real-ℚ x ≤ real-ℚ y
(#1303)
Build and deploy library website
#658:
Commit 5d2a1c2
pushed
by
fredrik-bakke
q : ℚ
is in the lower cut of a real only if real-ℚ q is less than t…
Build and deploy library website
#657:
Commit 304930a
pushed
by
fredrik-bakke
q : ℚ
is in the lower cut of a real, real-ℚ q
is less than tha…
Build and deploy library website
#653:
Commit 535aa73
pushed
by
fredrik-bakke
p q : ℚ
, succ-ℚ p * q = q + (p * q)
(#1282)
Build and deploy library website
#648:
Commit 8662d37
pushed
by
fredrik-bakke
ℝ
(#1275)
Build and deploy library website
#646:
Commit c6b929a
pushed
by
EgbertRijke
ℚ
(#1283)
Build and deploy library website
#645:
Commit f21dcf3
pushed
by
EgbertRijke
ℝ
(#1276)
Build and deploy library website
#643:
Commit eb58aa1
pushed
by
EgbertRijke