ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-tau GIF version

Definition df-tau 11922
Description: Define the circle constant tau, τ = 6.28318..., which is the smallest positive real number whose cosine is one. Various notations have been used or proposed for this number including τ, a three-legged variant of π, or . Note the difference between this constant τ and the formula variable 𝜏. Following our convention, the constant is displayed in upright font while the variable is in italic font; furthermore, the colors are different. (Contributed by Jim Kingdon, 9-Apr-2018.) (Revised by AV, 1-Oct-2020.)
Assertion
Ref Expression
df-tau τ = inf((ℝ+ ∩ (cos “ {1})), ℝ, < )

Detailed syntax breakdown of Definition df-tau
StepHypRef Expression
1 ctau 11921 . 2 class τ
2 crp 9722 . . . 4 class +
3 ccos 11791 . . . . . 6 class cos
43ccnv 4659 . . . . 5 class cos
5 c1 7875 . . . . . 6 class 1
65csn 3619 . . . . 5 class {1}
74, 6cima 4663 . . . 4 class (cos “ {1})
82, 7cin 3153 . . 3 class (ℝ+ ∩ (cos “ {1}))
9 cr 7873 . . 3 class
10 clt 8056 . . 3 class <
118, 9, 10cinf 7044 . 2 class inf((ℝ+ ∩ (cos “ {1})), ℝ, < )
121, 11wceq 1364 1 wff τ = inf((ℝ+ ∩ (cos “ {1})), ℝ, < )
Colors of variables: wff set class
This definition is referenced by:  taupi  15633
  Copyright terms: Public domain W3C validator