Whole Conditions and Characterization

SE.Individuation.Structural.Whole

An admissible presentation with support W succeeds exactly when:

1. nonemptiness: W contains an eligible atom;
2. internal co-membership: every two atoms in W are co-members;
3. saturation: every eligible atom co-member with an atom in W is in W.

These conditions characterize exactly one E-class of eligible atoms (wholeConditions_iff_isClass). The result uses only the equivalence-class structure of E, not the connectivity construction.

def SE.Individuation.Structural.Setting.WholeConditions {A Presentation : Type u} (s : Setting A Presentation) (W : MathlibMini.Set A) : Prop

The three whole conditions on a set of atoms.

Equations

• s.WholeConditions W = ((∃ (a : A), a ∈ W ∧ a ∈ s.eligible) ∧ (∀ (a b : A), a ∈ W → b ∈ W → s.CoMember a b) ∧ ∀ (a b : A), a ∈ W → b ∈ s.eligible → s.CoMember a b → b ∈ W)

def SE.Individuation.Structural.Setting.Succeeds {A Presentation : Type u} (s : Setting A Presentation) (p : Presentation) : Prop

A presentation succeeds when it is admissible and its support meets the whole conditions.

Equations

• s.Succeeds p = (s.admissible p ∧ s.WholeConditions (s.support p))

def SE.Individuation.Structural.Setting.IsClass {A Presentation : Type u} (s : Setting A Presentation) (W : MathlibMini.Set A) : Prop

W is the E-class of some eligible atom.

Equations

• s.IsClass W = ∃ (a : A), a ∈ s.eligible ∧ ∀ (b : A), b ∈ W ↔ s.CoMember a b

theorem SE.Individuation.Structural.Setting.wholeConditions_iff_isClass {A Presentation : Type u} (s : Setting A Presentation) (W : MathlibMini.Set A) : s.WholeConditions W ↔ s.IsClass W

The whole conditions characterize exactly one eligible E-class.

theorem SE.Individuation.Structural.Setting.WholeConditions.subset_eligible {A Presentation : Type u} {s : Setting A Presentation} {W : MathlibMini.Set A} (h : s.WholeConditions W) : W ⊆ s.eligible

Every set meeting the whole conditions lies inside the eligible domain.

theorem SE.Individuation.Structural.Setting.succeeds_iff_isClass {A Presentation : Type u} (s : Setting A Presentation) (p : Presentation) : s.Succeeds p ↔ s.admissible p ∧ s.IsClass (s.support p)

Success of an admissible presentation is exactly that its support is one eligible class.

theorem SE.Individuation.Structural.Setting.Succeeds.admissible {A Presentation : Type u} {s : Setting A Presentation} {p : Presentation} (h : s.Succeeds p) : s.admissible p

A presentation that succeeds is admissible.

theorem SE.Individuation.Structural.Setting.WholeConditions.eq_or_disjoint {A Presentation : Type u} {s : Setting A Presentation} {W₁ W₂ : MathlibMini.Set A} (h₁ : s.WholeConditions W₁) (h₂ : s.WholeConditions W₂) : W₁ = W₂ ∨ ∀ (a : A), a ∈ W₁ → ¬a ∈ W₂

Two sets meeting the whole conditions are equal or share no atom.

theorem SE.Individuation.Structural.Setting.WholeConditions.not_eq_and_disjoint {A Presentation : Type u} {s : Setting A Presentation} {W₁ W₂ : MathlibMini.Set A} (h₁ : s.WholeConditions W₁) : ¬(W₁ = W₂ ∧ ∀ (a : A), a ∈ W₁ → ¬a ∈ W₂)

Two sets meeting the whole conditions are not both equal and disjoint. Nonemptiness is what excludes the overlap of the two cases.