English
If a function is analytic near every point of a set s, then it is analytic on the entire set s.
Русский
Если функция аналитична в окрестности каждой точки множества s, то она аналитична на всем множестве s.
LaTeX
$$Let f : E → F be such that for every x ∈ s there exists an open u with x ∈ u and AnalyticOn 𝕜 f (s ∩ u). Then AnalyticOn 𝕜 f s.$$
Lean4
/-- If `f` is `AnalyticOn` near each point in a set, it is `AnalyticOn` the set -/
theorem analyticOn_of_locally_analyticOn {f : E → F} {s : Set E}
(h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)) : AnalyticOn 𝕜 f s :=
by
intro x m
rcases h x m with ⟨u, ou, xu, fu⟩
rcases Metric.mem_nhds_iff.mp (ou.mem_nhds xu) with ⟨r, r0, ru⟩
rcases fu x ⟨m, xu⟩ with ⟨p, t, fp⟩
exact
⟨p, min (.ofReal r) t,
{ r_pos := lt_min (by positivity) fp.r_pos
r_le := min_le_of_right_le fp.r_le
hasSum := by
intro y ys yr
simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at yr
apply fp.hasSum
· simp only [mem_insert_iff, add_eq_left] at ys
rcases ys with rfl | ys
· simp
· simp only [mem_insert_iff, add_eq_left, mem_inter_iff, ys, true_and]
apply Or.inr (ru ?_)
simp only [Metric.mem_ball, dist_self_add_left, yr]
· simp only [EMetric.mem_ball, yr] }⟩
