circle

Stream: mathlib4

[edklencl]

r : ℝ≥0
⊢ disc ↑r = regionBetween (fun x => -√(↑r ^ 2 - x ^ 2)) (fun x => √(↑r ^ 2 - x ^ 2)) (Ioc (-↑r) ↑r)

[edklencl]

what does the up arrow stand for

[edklencl]

this is the code from 100 theorem

[Daniel Weber]

It stands for a coercion (from the context it's probably from ℝ≥0 to ℝ)