Mathlib v3 is deprecated. Go to Mathlib v4

Theorem upper_half_plane.at_im_infty_basis

Modification history

2022-09-07 15:10

src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean

feat(analysis/complex/upper_half_plane): Functions bounded at infinity (#15009) …

Added upper_half_plane.at_im_infty_basis View on Github →