Theorems · Theorem · complex analysis

MeromorphicOn.meromorphicOn_closedBall_comp_sub_const_iff_meromorphicOn_closedBall

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicOn (f ∘ fun x => x - c) (Metric.closedBall c R) ↔ MeromorphicOn f (Metric.closedBall 0 R)

MeromorphicOn is invariant under translation, special case where the set is a closed ball.

Defined in: Mathlib.Analysis.Meromorphic.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NontriviallyNormedField NormedAddCommGroup NormedSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setproof · cited by 53,352
Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
NormedSpacestatement and proof · cited by 12,499
NontriviallyNormedFieldstatement and proof · cited by 8,742
sub_selfproof · cited by 996
Metric.closedBallstatement and proof · cited by 704
MeromorphicOnstatement and proof · cited by 141
MeromorphicOn.meromorphicOn_comp_sub_const_iff_meromorphicOnproof · cited by 4
closedBall_sub_singletonproof · cited by 4

Cited by1

Results whose statement or proof uses this declaration.

MeromorphicOn.meromorphicOn_closedBall_fun_comp_sub_const_iff_meromorphicOn_closedBallproof · cited by 0