Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-inftyexpi Structured version   Visualization version   GIF version

Definition df-bj-inftyexpi 34570
 Description: Definition of the auxiliary function +∞ei parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with ℂ to simplify the proof of bj-ccinftydisj 34576. It could seem more natural to define +∞ei on all of ℝ, but we want to use only basic functions in the definition of ℂ̅. TODO: transition to df-bj-inftyexpitau 34562 instead. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)
Assertion
Ref Expression
df-bj-inftyexpi +∞ei = (𝑥 ∈ (-π(,]π) ↦ ⟨𝑥, ℂ⟩)

Detailed syntax breakdown of Definition df-bj-inftyexpi
StepHypRef Expression
1 cinftyexpi 34569 . 2 class +∞ei
2 vx . . 3 setvar 𝑥
3 cpi 15420 . . . . 5 class π
43cneg 10869 . . . 4 class
5 cioc 12736 . . . 4 class (,]
64, 3, 5co 7149 . . 3 class (-π(,]π)
72cv 1537 . . . 4 class 𝑥
8 cc 10533 . . . 4 class
97, 8cop 4556 . . 3 class 𝑥, ℂ⟩
102, 6, 9cmpt 5132 . 2 class (𝑥 ∈ (-π(,]π) ↦ ⟨𝑥, ℂ⟩)
111, 10wceq 1538 1 wff +∞ei = (𝑥 ∈ (-π(,]π) ↦ ⟨𝑥, ℂ⟩)
 Colors of variables: wff setvar class This definition is referenced by:  bj-inftyexpiinv  34571  bj-inftyexpidisj  34573  bj-ccinftydisj  34576  bj-elccinfty  34577  bj-minftyccb  34588
 Copyright terms: Public domain W3C validator