Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.nhds_hasBasis_square

PrimeNumberTheoremAnd.Rectangle · PrimeNumberTheoremAnd/Rectangle.lean:253 to 264

Mathematical statement

Exact Lean statement

theorem Complex.nhds_hasBasis_square (p : ℂ) : (𝓝 p).HasBasis (0 < ·) (Square p ·)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem Complex.nhds_hasBasis_square (p : ℂ) : (𝓝 p).HasBasis (0 < ·) (Square p ·) := by  suffices      (𝓝 p.re ×ˢ 𝓝 p.im).HasBasis (0 < ·)        (equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p ·)    by simpa only [← nhds_prod_eq, Homeomorph.map_nhds_eq, Homeomorph.image_preimage]      using! this.map equivRealProdCLM.symm.toHomeomorph  apply ((nhds_basis_Icc_pos p.re).prod_same_index_mono (nhds_basis_Icc_pos p.im) ?_ ?_).congr  · intro; rfl  · intros    rw [← uIcc_of_lt (by linarith), ← uIcc_of_lt (by linarith)]    simpa [Square, Rectangle] using by ring_nf  all_goals exact (antitone_const_tsub.Icc (monotone_id.const_add _)).monotoneOn _