Natural selections from families of sets

A selection rule picks a set of labels from any family of sets of labels. It is natural when it commutes with every relabeling whose preimage carries one antichain bijectively onto another, and consistent when on a finite nonempty antichain it picks within some member. Taking the intersection is natural and consistent, and every natural consistent rule picks within it, while choosing one member is consistent but not natural. So on a finite antichain the intersection is the greatest set a natural consistent rule selects; in particular the elements in every maximal set meeting a condition are the greatest such selection from those maximal sets.

Main definitions

• Set.IsNaturalSelection, Set.IsConsistentSelection

Main statements

• Set.isGreatest_sInter: on a finite antichain, the intersection is the greatest set a natural consistent rule selects.
• Set.not_isNaturalSelection_choose: choosing a member is not natural.

Implementation notes

The rule is a family F : ∀ A : Type u, Set (Set A) → Set A over all label types, so that naturality can compare a family with its copies in larger types. The upper bound comes from a cyclic cover: the family N 0, …, N n sits inside copies A × Fin (n + 1) whose shift permutes the members cyclically, so a natural rule that picks a label outside some member picks every copy of it, and no member of the cover then contains its pick.

def Set.IsNaturalSelection (F : (A : Type u) → Set (Set A) → Set A) : Prop

A selection rule is natural when it commutes with every relabeling whose preimage carries one antichain bijectively onto another.

Equations

• One or more equations did not get rendered due to their size.

def Set.IsConsistentSelection (F : (A : Type u) → Set (Set A) → Set A) : Prop

A selection rule is consistent when on every finite nonempty antichain it selects within some member.

Equations

• Set.IsConsistentSelection F = ∀ ⦃A : Type ?u.1⦄ ⦃𝓚 : Set (Set A)⦄, IsAntichain (fun (x1 x2 : Set A) => x1 ⊆ x2) 𝓚 → 𝓚.Finite → 𝓚.Nonempty → ∃ K ∈ 𝓚, F A 𝓚 ⊆ K

The cyclic cover

The intersection is the greatest natural consistent selection

theorem Set.IsNaturalSelection.subset_sInter {F : (A : Type u) → Set (Set A) → Set A} (hnat : IsNaturalSelection F) (hcons : IsConsistentSelection F) {A : Type u} {𝓚 : Set (Set A)} (h𝓚 : IsAntichain (fun (x1 x2 : Set A) => x1 ⊆ x2) 𝓚) (hfin : 𝓚.Finite) : F A 𝓚 ⊆ ⋂₀ 𝓚

A natural consistent rule selects from a finite antichain only labels in every member.

theorem Set.isNaturalSelection_sInter : IsNaturalSelection fun (A : Type u_1) (𝓚 : Set (Set A)) => ⋂₀ 𝓚

Selecting the intersection is natural.

theorem Set.isConsistentSelection_sInter : IsConsistentSelection fun (A : Type u_1) (𝓚 : Set (Set A)) => ⋂₀ 𝓚

Selecting the intersection is consistent.

theorem Set.isGreatest_sInter {A : Type u} {𝓚 : Set (Set A)} (h𝓚 : IsAntichain (fun (x1 x2 : Set A) => x1 ⊆ x2) 𝓚) (hfin : 𝓚.Finite) : IsGreatest ((fun (F : (A : Type u) → Set (Set A) → Set A) => F A 𝓚) '' {F : (A : Type u) → Set (Set A) → Set A | IsNaturalSelection F ∧ IsConsistentSelection F}) (⋂₀ 𝓚)

On a finite antichain, the intersection is the greatest set a natural consistent rule selects.

theorem Set.not_isNaturalSelection_choose : ¬IsNaturalSelection fun (x : Type) (𝓚 : Set (Set x)) => if h : 𝓚.Nonempty then h.some else ∅

Choosing a member of the family is consistent but not natural, since on two disjoint options it selects one of them, outside their intersection.

theorem Set.isGreatest_setOf_forall_maximal {α : Type u} {s : Set α} {P : Set α → Prop} (hs : s.Finite) (hP : ∀ (X : Set α), P X → X ⊆ s) (hne : ∃ (X : Set α), P X) : IsGreatest ((fun (F : (A : Type u) → Set (Set A) → Set A) => F α {X : Set α | Maximal P X}) '' {F : (A : Type u) → Set (Set A) → Set A | IsNaturalSelection F ∧ IsConsistentSelection F}) {a : α | a ∈ s ∧ ∀ (X : Set α), Maximal P X → a ∈ X}

When a condition holds of some subset of a finite set s and only of subsets of s, the elements of s in every maximal set meeting it are the greatest set a natural consistent rule selects from those maximal sets.