Density from one-dimensional analytic nonvanishing

This file packages the isolated-zero argument used in Poincaré's perturbing-function calculation. A real-analytic function on a connected open set that is nonzero at one point is nonzero on a dense subset of that set.

theorem LeanPool.PoincareThreeBody.dense_nonzero_of_analyticOnNhd {f : ℝ → ℝ} {U : Set ℝ} (hUopen : IsOpen U) (hUconnected : IsConnected U) (hf : AnalyticOnNhd ℝ f U) {witness : ℝ} (hwitness : witness ∈ U) (hfwitness : f witness ≠ 0) : Dense {x : ↑U | f ↑x ≠ 0}

The nonzero locus of a nontrivial real-analytic function is dense in any connected open domain. The set is regarded as a subset of the domain subtype.