LeanPool.Rupert.Convex

Imported Lean Pool material for LeanPool.Rupert.Convex.

@[reducible, inline]

abbrev Convex.E (n : ℕ) : Type

n-dimensional Euclidean space over ℝ, indexed by Fin n.

Equations

• Convex.E n = EuclideanSpace ℝ (Fin n)

theorem Convex.move_scale {n : ℕ} {s : ℝ} (sgz : s > 0) {v : E n} {Y : Set (E n)} : v ∈ s • Y → (1 / s) • v ∈ Y

theorem Convex.subset_interior_hull' {n : ℕ} {X : Set (E n)} {ε ℓ : ℝ} (hε : 0 < ε) (hℓ : ℓ ∈ Set.Ioo 0 1) (h0 : Metric.ball 0 ε ⊆ X) : ℓ • X ⊆ interior ((convexHull ℝ) X)

theorem Convex.subset_interior_hull {n : ℕ} {X : Set (E n)} {ε₀ ε₁ : ℝ} (hε₀ : 0 < ε₀) (hε₁ : ε₁ ∈ Set.Ioo 0 1) (h0 : Metric.ball 0 ε₀ ⊆ (convexHull ℝ) X) : (convexHull ℝ) ((1 - ε₁) • X) ⊆ interior ((convexHull ℝ) X)

theorem Convex.mem_interior_hull {n : ℕ} {X : Set (E n)} {ε₀ ε₁ : ℝ} (hε₀ : 0 < ε₀) (hε₁ : ε₁ ∈ Set.Ioo 0 1) (h0 : Metric.ball 0 ε₀ ⊆ (convexHull ℝ) X) {p : E n} (h : p ∈ (convexHull ℝ) ((fun (v : E n) => (1 - ε₁) • v) '' X)) : p ∈ interior ((convexHull ℝ) X)

theorem Convex.ball_in_hull_of_corners_in_hull {X : Set (E 2)} {ε : ℝ} (hε : ε ∈ Set.Ioo 0 1) (h₀ : !₂[ε, ε] ∈ (convexHull ℝ) X) (h₁ : !₂[-ε, ε] ∈ (convexHull ℝ) X) (h₂ : !₂[-ε, -ε] ∈ (convexHull ℝ) X) (h₃ : !₂[ε, -ε] ∈ (convexHull ℝ) X) : Metric.ball 0 ε ⊆ (convexHull ℝ) X