bookshelf/Bookshelf/Real/Basic.lean

30 lines
504 B
Plaintext
Raw Normal View History

import Mathlib.Data.Real.Basic
2023-05-04 22:37:54 +00:00
/-! # Bookshelf.Real.Basic
A collection of basic notational conveniences.
-/
/--
An abbreviation of `ℝ²` as the Cartesian product ` × `.
-/
notation "ℝ²" => ×
namespace Real
/--
2023-05-04 22:37:54 +00:00
Definitionally, the area of a unit circle.
###### PORT
As of now, this remains an `axiom`, but it should be replaced by the definition
in `Mathlib` once ported to Lean 4.
-/
axiom pi :
2023-05-04 22:37:54 +00:00
/--
An abbreviation of `pi` as symbol `π`.
-/
notation "π" => pi
end Real