English
If a HasFPowerSeriesWithinAt f p s x holds and s is in nhdsWithin x t, then HasFPowerSeriesWithinAt f p t x holds.
Русский
Если HasFPowerSeriesWithinAt для s в nhdsWithin x и s принадлежит nhdsWithin x t, то HasFPowerSeriesWithinAt верно и для t.
LaTeX
$$$HasFPowerSeriesWithinAt\\; f p s x \\to (s \\in 𝓝[t] x) \\Rightarrow HasFPowerSeriesWithinAt f p t x$$$
Lean4
theorem mono_of_mem_nhdsWithin (h : HasFPowerSeriesWithinAt f p s x) (hst : s ∈ 𝓝[t] x) :
HasFPowerSeriesWithinAt f p t x := by
rcases h with ⟨r, hr⟩
rcases EMetric.mem_nhdsWithin_iff.1 hst with ⟨r', r'_pos, hr'⟩
refine ⟨min r r', ?_⟩
have Z := hr.of_le (by simp [r'_pos, hr.r_pos]) (min_le_left r r')
refine ⟨Z.r_le, Z.r_pos, fun {y} hy h'y ↦ ?_⟩
apply Z.hasSum ?_ h'y
simp only [mem_insert_iff, add_eq_left] at hy
rcases hy with rfl | hy
· simp
apply mem_insert_of_mem _ (hr' ?_)
simp only [EMetric.mem_ball, edist_eq_enorm_sub, sub_zero, lt_min_iff, mem_inter_iff, add_sub_cancel_left, hy,
and_true] at h'y ⊢
exact h'y.2
