Description: Definition of infty , the point at infinity of the real or complex projective line. (Contributed by BJ, 27-Jun-2019) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-bj-infty | ⊢ ∞ = 𝒫 ∪ ℂ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cinfty | ⊢ ∞ | |
| 1 | cc | ⊢ ℂ | |
| 2 | 1 | cuni | ⊢ ∪ ℂ |
| 3 | 2 | cpw | ⊢ 𝒫 ∪ ℂ |
| 4 | 0 3 | wceq | ⊢ ∞ = 𝒫 ∪ ℂ |