theorem HexRootsMathlib.continuous_circleIntegral {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℂ E] {f : X → ℂ → E} (c : ℂ) (R : ℝ) (hf : Continuous fun (q : X × ℝ) => f q.1 (circleMap c R q.2)) : Continuous fun (x : X) => ∮ (z : ℂ) in C(c, R), f x z

A fixed-circle integral varies continuously when the integrand restricted to the parameter-times-circle parametrization is jointly continuous.

theorem HexRootsMathlib.continuous_circleIntegral_div {X : Type u_1} [TopologicalSpace X] {f g : X → ℂ → ℂ} (c : ℂ) (R : ℝ) (hf : Continuous fun (q : X × ℝ) => f q.1 (circleMap c R q.2)) (hg : Continuous fun (q : X × ℝ) => g q.1 (circleMap c R q.2)) (hzero : ∀ (q : X × ℝ), g q.1 (circleMap c R q.2) ≠ 0) : Continuous fun (x : X) => ∮ (z : ℂ) in C(c, R), f x z / g x z

A fixed-circle integral of a quotient varies continuously if numerator and denominator are jointly continuous on the parameterized circle and the denominator never vanishes there.

theorem HexRootsMathlib.continuousOn_circleIntegral_div {X : Type u_1} [TopologicalSpace X] {f g : X → ℂ → ℂ} {s : Set X} (c : ℂ) (R : ℝ) (hf : ContinuousOn (fun (q : X × ℝ) => f q.1 (circleMap c R q.2)) (s ×ˢ Set.univ)) (hg : ContinuousOn (fun (q : X × ℝ) => g q.1 (circleMap c R q.2)) (s ×ˢ Set.univ)) (hzero : ∀ x ∈ s, ∀ (θ : ℝ), g x (circleMap c R θ) ≠ 0) : ContinuousOn (fun (x : X) => ∮ (z : ℂ) in C(c, R), f x z / g x z) s

A fixed-circle integral of a quotient varies continuously on a parameter set when the data are jointly continuous and the denominator is nonzero only over that set.

theorem HexRootsMathlib.continuousOn_normalizedCircleIntegral_div {X : Type u_1} [TopologicalSpace X] {f g : X → ℂ → ℂ} {s : Set X} (c : ℂ) (R : ℝ) (hf : ContinuousOn (fun (q : X × ℝ) => f q.1 (circleMap c R q.2)) (s ×ˢ Set.univ)) (hg : ContinuousOn (fun (q : X × ℝ) => g q.1 (circleMap c R q.2)) (s ×ˢ Set.univ)) (hzero : ∀ x ∈ s, ∀ (θ : ℝ), g x (circleMap c R θ) ≠ 0) : ContinuousOn (fun (x : X) => (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(c, R), f x z / g x z) s

The normalized integral of a quotient varies continuously on a parameter set under a nonvanishing hypothesis restricted to that set.

theorem HexRootsMathlib.continuousOn_nat_of_cast {X : Type u_1} [TopologicalSpace X] {f : X → ℕ} {s : Set X} (hf : ContinuousOn (fun (x : X) => ↑(f x)) s) : ContinuousOn f s

Continuity on a set of a real cast detects continuity on that set of a natural-valued map.

theorem HexRootsMathlib.continuousOn_nat_of_complexCast {X : Type u_1} [TopologicalSpace X] {f : X → ℕ} {s : Set X} (hf : ContinuousOn (fun (x : X) => ↑(f x)) s) : ContinuousOn f s

Continuity on a set of a complex cast detects continuity on that set of a natural-valued map.

theorem HexRootsMathlib.continuousOn_int_of_cast {X : Type u_1} [TopologicalSpace X] {f : X → ℤ} {s : Set X} (hf : ContinuousOn (fun (x : X) => ↑(f x)) s) : ContinuousOn f s

Continuity on a set of a real cast detects continuity on that set of an integer-valued map.

theorem HexRootsMathlib.continuousOn_int_of_complexCast {X : Type u_1} [TopologicalSpace X] {f : X → ℤ} {s : Set X} (hf : ContinuousOn (fun (x : X) => ↑(f x)) s) : ContinuousOn f s

Continuity on a set of a complex cast detects continuity on that set of an integer-valued map.

theorem HexRootsMathlib.eq_endpoints_of_continuousOn {Y : Type u_1} [TopologicalSpace Y] [DiscreteTopology Y] {a b : ℝ} (hab : a ≤ b) {f : ℝ → Y} (hf : ContinuousOn f (Set.Icc a b)) : f a = f b

A continuous map from a real interval to a discrete space has equal values at its endpoints.

theorem HexRootsMathlib.nat_eq_endpoints_of_complexCast {a b : ℝ} (hab : a ≤ b) {f : ℝ → ℕ} (hf : ContinuousOn (fun (x : ℝ) => ↑(f x)) (Set.Icc a b)) : f a = f b

A natural-valued map has equal endpoint values when its complex cast is continuous on the intervening interval.

This packaged form is the module's stated terminus; the Rouché homotopy development applies the two halves (continuousOn_nat_of_complexCast, eq_endpoints_of_continuousOn) separately because it names the intermediate continuity statement continuous_rootsInDisc.

theorem HexRootsMathlib.int_eq_endpoints_of_complexCast {a b : ℝ} (hab : a ≤ b) {f : ℝ → ℤ} (hf : ContinuousOn (fun (x : ℝ) => ↑(f x)) (Set.Icc a b)) : f a = f b

An integer-valued map has equal endpoint values when its complex cast is continuous on the intervening interval.

Integer-valued counterpart of nat_eq_endpoints_of_complexCast, kept as the module's general winding-number-valued terminus.