LeanPool.RiemannMappingTheorem.ToMathlib

theorem isCompact_segment {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [CompactIccSpace 𝕜] [TopologicalSpace E] [AddCommGroup E] [ContinuousAdd E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {x y : E} : IsCompact (segment 𝕜 x y)

theorem DifferentiableAt.deriv_eq_deriv_pow_div_pow {z : ℂ} {n : ℕ} (n_pos : 0 < n) {f g : ℂ → ℂ} (hg : ∀ᶠ (z : ℂ) in nhds z, f z = g z ^ n) (g_diff : DifferentiableAt ℂ g z) (fz_nonzero : f z ≠ 0) : deriv g z = deriv f z / (↑n * g z ^ (n - 1))

theorem has_deriv_at_integral_of_continuous_of_lip {φ : ℂ → ℝ → ℂ} {ψ : ℝ → ℂ} {z₀ : ℂ} {a b C δ : ℝ} (hab : a ≤ b) (δ_pos : 0 < δ) (φ_cts : ∀ᶠ (z : ℂ) in nhds z₀, ContinuousOn (φ z) (Set.Icc a b)) (φ_der : ∀ t ∈ Set.Ioc a b, HasDerivAt (fun (x : ℂ) => φ x t) (ψ t) z₀) (φ_lip : ∀ t ∈ Set.Ioc a b, LipschitzOnWith (Real.nnabs C) (fun (x : ℂ) => φ x t) (Metric.ball z₀ δ)) (ψ_cts : ContinuousOn ψ (Set.Ioc a b)) : HasDerivAt (fun (z : ℂ) => ∫ (t : ℝ) in a..b, φ z t) (∫ (t : ℝ) in a..b, ψ t) z₀

theorem uIoo_eq_union {a b : ℝ} : Set.uIoo a b = Set.Ioo a b ∪ Set.Ioo b a

theorem mem_uIoo {a b t : ℝ} : t ∈ Set.uIoo a b ↔ a < t ∧ t < b ∨ b < t ∧ t < a

theorem uIoo_eq_uIoc_sdiff_ends {a b : ℝ} : Set.uIoo a b = Set.uIoc a b \ {a, b}

theorem uIoo_eq_uIcc_sdiff_ends {a b : ℝ} : Set.uIoo a b = Set.uIcc a b \ {a, b}

theorem uIcc_mem_nhds {a b t : ℝ} (h : t ∈ Set.uIoo a b) : Set.uIcc a b ∈ nhds t

theorem uIcc_mem_nhds_within {a b t : ℝ} (h : t ∈ Set.uIoo a b) : Set.uIcc a b ∈ nhdsWithin t (Set.Ioi t)

theorem eventually_mem_uIoo_of_mem_uIoc {a b : ℝ} : ∀ᵐ (x : ℝ), x ∈ Set.uIoc a b → x ∈ Set.uIoo a b

theorem derivWithin_of_mem_uIoo {E : Type u_2} {a b t : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (ht : t ∈ Set.uIoo a b) : derivWithin f (Set.uIcc a b) t = deriv f t

theorem intervalIntegral.integral_congr_uIoo' {E : Type u_2} {a b : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} (h : Set.EqOn f g (Set.uIoo a b)) : ∫ (t : ℝ) in a..b, f t = ∫ (t : ℝ) in a..b, g t

theorem ContDiffOn.continuousOn_derivWithin'' {E : Type u_2} {a b : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {n : ℕ∞} (h : ContDiffOn ℝ (↑n) f (Set.uIcc a b)) (hn : 1 ≤ n) : ContinuousOn (derivWithin f (Set.uIcc a b)) (Set.uIcc a b)

theorem ContDiffOn.integral_eq_sub' {E : Type u_2} {a b : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (h : ContDiffOn ℝ 1 f (Set.Icc a b)) (hab : a < b) : ∫ (y : ℝ) in a..b, derivWithin f (Set.Icc a b) y = f b - f a

theorem ContDiffOn.integral_eq_sub {E : Type u_2} {a b : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (h : ContDiffOn ℝ 1 f (Set.Icc a b)) (hab : a ≤ b) : ∫ (y : ℝ) in a..b, derivWithin f (Set.Icc a b) y = f b - f a

theorem ContDiffOn.integral_derivWithin_smul_comp {E : Type u_2} {a b : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {g : ℝ → ℝ} (hg : ContDiffOn ℝ 1 g (Set.uIcc a b)) (hf : ContinuousOn f (g '' Set.uIcc a b)) : ∫ (x : ℝ) in a..b, derivWithin g (Set.uIcc a b) x • (f ∘ g) x = ∫ (x : ℝ) in g a..g b, f x

theorem ContDiffOn.integral_eq_sub''' {E : Type u_2} {a b : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (h : ContDiffOn ℝ 1 f (Set.Icc a b)) (hab : a ≤ b) : ∫ (y : ℝ) in a..b, deriv f y = f b - f a

theorem ContDiffOn.integral_eq_sub_u {E : Type u_2} {a b : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (h : ContDiffOn ℝ 1 f (Set.uIcc a b)) : ∫ (y : ℝ) in a..b, deriv f y = f b - f a

theorem ContDiffOn.integral_eq_sub'' {E : Type u_2} {a b t : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (h : ContDiffOn ℝ 1 f (Set.Icc a b)) (hab : a ≤ b) (ht : t ∈ Set.Icc a b) : ∫ (y : ℝ) in a..t, derivWithin f (Set.Icc a b) y = f t - f a

theorem exists_div_lt (a : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ (n : ℕ), a / ↑(n + 1) < ε

theorem List.Pairwise.ext {α : Type u_4} [LinearOrder α] {l1 l2 : List α} (h1 : Pairwise (fun (x1 x2 : α) => x1 ≤ x2) l1) (h2 : Pairwise (fun (x1 x2 : α) => x1 ≤ x2) l2) (h'1 : l1.Nodup) (h'2 : l2.Nodup) (h : ∀ (x : α), x ∈ l1 ↔ x ∈ l2) : l1 = l2

theorem List.Pairwise.ext' {α : Type u_4} [LinearOrder α] {l1 l2 : List α} (h1 : Pairwise (fun (x1 x2 : α) => x1 < x2) l1) (h2 : Pairwise (fun (x1 x2 : α) => x1 < x2) l2) (h4 : ∀ (x : α), x ∈ l1 ↔ x ∈ l2) : l1 = l2

@[simp]

theorem List.Pairwise.toFinset_sort {α : Type u_4} [LinearOrder α] {l : List α} (hl : Pairwise (fun (x1 x2 : α) => x1 < x2) l) : (l.toFinset.sort fun (x1 x2 : α) => x1 ≤ x2) = l