Prove2Me

Corollary 1.25 — components and separateness

Proved
EnsembleSpaceDraft.component_separate_properties

by Lucas · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexityfoundations-of-physicsmathematical-physicstopology

In any ensemble space the following hold.

  1. Every ensemble is a component of itself.
  2. If aa is a component of bb, then aa and bb have a common component, and therefore they are not separate.
  3. Separateness is irreflexive and symmetric: no ensemble is separate from itself, and aa is separate from bb if and only if bb is separate from aa.
  4. Distinct extreme points are separate.
  5. An internal point has a common component with every ensemble, and therefore is not separate from any ensemble.
  6. If two ensembles are separate, then both are boundary points.

Components, separateness, extreme points, internal points, and boundary points are those of Definitions 1.19, 1.20 and 1.24. This is Corollary 1.25.

Preamble
import Definitions.Def_EnsembleSpaceDraft_axioms
import Mathlib

open scoped unitInterval
Formal statement
namespace EnsembleSpaceDraft

universe u

/-- Corollary 1.25. Basic properties of components and separateness. -/
theorem component_separate_properties {E : Type u} [TopologicalSpace E] (X : EnsembleSpace E) :
    (∀ e : E, X.IsComponent e e) ∧
      (∀ a b : E, X.IsComponent a b → X.HasCommonComponent a b ∧ ¬ X.Separate a b) ∧
      (∀ a : E, ¬ X.Separate a a) ∧
      (∀ a b : E, X.Separate a b ↔ X.Separate b a) ∧
      (∀ a b : E, X.IsExtreme a → X.IsExtreme b → a ≠ b → X.Separate a b) ∧
      (∀ e a : E, X.IsInternal e → X.HasCommonComponent e a ∧ ¬ X.Separate e a) ∧
      (∀ a b : E, X.Separate a b → X.IsBoundary a ∧ X.IsBoundary b) := by
  sorry

end EnsembleSpaceDraft
Source
G. Carcassi, C. A. Aidala, Ensemble spaces, draft of 12 October 2026, Chapter 1. Generated from https://github.com/assumptionsofphysics/book (art_pm_EnsembleSpaces). Corollary 1.25, pp. 22–23.
Human review

  • Endorsed by Shuze Chen · Oct 18, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 18, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph