MATHLIBANNEX / CANONICAL DECLARATION CARD

A common generator selected from equal convex hulls

MathlibAnnex.exists_common_of_convexHull_eq

theorem

Uses a first maximizing slice and a separating sequence to obtain an original common point carrying a prescribed property.

Statement

Let be nonempty compact subsets of a finite-dimensional real normed space with . Let be a finite ordered list of continuous linear functionals that separates points of the ambient space. Fix another continuous linear functional and a property such that every maximizer of in satisfies . Then there exists with .

Assumptions

Point separation means that if for every functional in the list, then . The property is arbitrary; no continuity or closedness is assumed for it. It is required on every point of the maximum slice of for . Both original sets are nonempty compact, their convex hulls agree, and the ambient space is finite-dimensional over the reals.

Conclusion

The point belongs to both original generating sets and has the prescribed property. The proof obtains it in the first maximum slice of , which is what permits the final application of the assumption on .

For a finite real coordinate space, take the coordinate projections in any enumeration. Equality under every projection is equality of all coordinates, so this list separates points. The cited coordinate specialization supplies the same common-generator conclusion without asking the caller to construct a separating list.

Proof route

Equal convex hulls give equal maximum values and equal convex hulls after every refinement. The separating list makes a final refined set a singleton; its common convex hull then forces the same surviving original point on both sides.

Proof steps

  1. For any continuous linear functional , a bound on is preserved by convex combinations. Since and the maximum is attained in , this gives

    Apply this with , and call the common value . Let and . The support-face identity then gives

  2. Write the separating list as . Given nonempty compact with equal convex hulls, Step 1 supplies the same maximum

    Set and . These sets are nonempty compact. The support-face identity gives

    Induction gives this equality at every stage. For and it yields

    The maximum used at stage is taken on the preceding retained sets, not on the original .

  3. Two survivors in have equal values under every functional in the list: at the stage for a functional, both lie on that stage’s maximum level, and later stages only remove points. Point separation therefore makes any two survivors equal. Since is nonempty, choose and conclude . Choose . Then

    so . The inclusions from the previous step show that this same point belongs to and .

  4. Moreover , the initial maximum slice for . The hypothesis on that slice yields . Setting proves the full conclusion, including the property. An empty separating list is allowed only when its separation condition holds, in which case the ambient space has at most one point and the same argument still applies.

Main citations

Lean source signature (exact)

theorem exists_common_of_convexHull_eq [FiniteDimensional ℝ E]
    (ls : List (E →L[ℝ] ℝ))
    (hsep : ∀ x y : E, (∀ ℓ ∈ ls, ℓ x = ℓ y) → x = y)
    (K L : TopologicalSpace.NonemptyCompacts E)
    (hHull : convexHull ℝ (K : Set E) = convexHull ℝ (L : Set E))
    (ℓ : E →L[ℝ] ℝ)
    (Good : E → Prop)
    (hgood : ∀ z ∈ maxSlice L ℓ, Good z) :
    ∃ z, z ∈ (K : Set E) ∧ z ∈ (L : Set E) ∧ Good z
In the source Mathematical meaning
[FiniteDimensional ℝ E] The ambient real normed space is finite-dimensional, with its normed-space binders in the separate exact context.
(ls : List (E →L[ℝ] ℝ)) The finite ordered list of continuous real-linear functionals.
(hsep : ∀ x y : E, (∀ ℓ ∈ ls, ℓ x = ℓ y) → x = y) Point separation: if for every in the list, then .
(K L : TopologicalSpace.NonemptyCompacts E) (hHull : convexHull ℝ (K : Set E) = convexHull ℝ (L : Set E)) The original nonempty compact sets satisfy .
(ℓ : E →L[ℝ] ℝ) (Good : E → Prop) The additional functional and arbitrary point property .
In the source Mathematical meaning
(hgood : ∀ z ∈ maxSlice L ℓ, Good z) The input assumption: every with satisfies .
∃ z, z ∈ (K : Set E) ∧ z ∈ (L : Set E) ∧ Good z The conclusion supplies one and the same point satisfying ; membership is in the original sets, not just their convex hulls.
Exact surrounding binder context (separate excerpt) 
noncomputable section

open Set
open TopologicalSpace

namespace MathlibAnnex

universe u

variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.exists_common_of_convexHull_eq

Accepted content SHA-256: 186aa41ab8d1e99bcfd35e3c06411f17c94c55ab94d9e59d5ff5725fbdd783a8

Accepted source guide SHA-256: e60e678a126d7010d305842cd57f9657029df77d7b0cc816f889b35d60c37877

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑