OrderedSections.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

LeastOccurrence

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.At line 20
Source documentation
Occurrence at this index and forced nonoccurrence at every smaller index in the fixed ground wellordering.
```
def At (p : P) (x : S.Name) (i : X) : Prop :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.mono line 24
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.congr line 28
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.unique line 37
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.predicate line 43
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.dense line 56
Source documentation
Minimal compatible occurrence exists densely.
```
theorem dense (x : S.Name) (p : P)
    (h : ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ i, (R i).holds r x) :
    ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ i, At X R r x i := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.At
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.move line 67
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.relation line 83
Source documentation
The least-index graph, regularized in both the value and index names.
```
def relation : S.BinaryRelation where
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.relation_one line 104
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.relation_inj line 114
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.relation_move line 129

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.LeastOccurrence.exists_injection line 140

Source documentation

Every family of regular occurrences covering a set and with at most one value at each index supplies an internal injection into the ground index set.

theorem exists_injection (Y : S.Name) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hY : ∀ g ∈ H, g • Y = Y)
    (hR : ∀ g ∈ H, ∀ i p x, (R i).holds p x → (R i).holds (S.move g p) (g • x))
    (p : P)
    (hcover : ∀ x q, q ≤ p → S.atomic.MemF q x Y →
      ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ i, (R i).holds s x)
    (hone : ∀ i q, q ≤ p → ∀ x y, (R i).holds q x → (R i).holds q y → S.atomic.EqF q x y) :
    ∃ f : S.Name, S.Forces ![f,Y,Name.check X] p (SetLanguage.injection 0 1 2) := by
…

Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.injection

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.wellorderable_check_dense line 173
Source documentation
Dense presentation of a wellorderability witness by a ground ordinal.
```
theorem wellorderable_check_dense (X : S.Name) (p : P)
    (h : S.Forces ![X] p (SetLanguage.wellorderable 0)) :
    ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ β : Ordinal.{u}, ∃ J : S.Name,
      S.Forces ![J,X,Name.check β.toZFSet] r (SetLanguage.injection 0 1 2) := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.wellorderable, OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.injection
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedImage line 192
Source documentation
The value of a function at the (at most one) point of a given ordinal index in an injection of its domain.
```
def indexedImage (f J X Y : S.Name) (Ξ : ZFSet.{u}) (i : Ξ) : S.UnaryRelation where
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedImage_move line 199
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedImage_one line 211
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedImage_cover line 228
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.wellorderable_image line 249
Source documentation
Images of wellorderable sets are wellorderable, by least preimages, not by a use of Choice.
```
theorem wellorderable_image (f X Y : S.Name) (p : P)
    (hf : S.Forces ![f,X,Y] p (SetLanguage.surjection 0 1 2))
    (hX : S.Forces ![X] p (SetLanguage.wellorderable 0)) :
    S.Forces ![Y] p (SetLanguage.wellorderable 0) := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.wellorderable
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.familyUnion line 286
Source documentation
Regular union of an arbitrary indexed family of binary relations. The bounded graph constructor subsequently makes this relation an actual set.
```
def familyUnion {ι : Sort i} (R : ι → S.BinaryRelation) : S.BinaryRelation where
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.familyUnion_move line 305
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.atLeft line 313
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.atRight line 319
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UnaryRelation.member line 325
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UnaryRelation.neg line 331
def OAI.PartitionConsistency.SetLanguage.indexedSection line 354
Source documentation
A preimage for the (possibly absent) value at one ordinal index.
```
def indexedSection : Formula 6 :=
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_indexedSection line 365
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedSection_exists line 377
Source documentation
One fiber can be chosen without any simultaneous use of choice; an unoccupied ordinal index imposes no requirement on the selected name.
```
theorem indexedSection_exists (f X Y J O i : S.Name) (p : P)
    (hf : S.Forces ![f,X,Y] p (SetLanguage.surjection 0 1 2))
    (hJ : S.Forces ![J,Y,O] p (SetLanguage.injection 0 1 2)) :
    S.Forces ![f,X,Y,J,i] p SetLanguage.indexedSection.ex := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.injection
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.sectionPart line 408
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.sectionPart_move line 419

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.section_injection_of_uniform line 430

Source documentation

A uniformly supported collection of local preimages gives one internal injection, including its totality and its absence of extraneous graph entries.

theorem section_injection_of_uniform (f X Y J : S.Name) (Ξ : ZFSet.{u}) (c : Ξ → S.Name)
    (H : Subgroup Γ) (hH : H ∈ S.filter) (hX : ∀ g ∈ H, g • X = X)
    (hY : ∀ g ∈ H, g • Y = Y) (hJ : ∀ g ∈ H, g • J = J)
    (hc : ∀ g ∈ H, ∀ i, g • c i = c i) (p : P)
    (hf : S.Forces ![f,X,Y] p (SetLanguage.mapsTo 0 1 2))
    (hj : S.Forces ![J,Y,Name.check Ξ] p (SetLanguage.mapsTo 0 1 2))
    (hs : ∀ i y q, q ≤ p → S.atomic.MemF q y Y → S.App q J y (Name.check i.val) →
      S.atomic.MemF q (c i) X ∧ S.App q f (c i) y) :
    ∃ K : S.Name, S.Forces ![K,Y,X] p (SetLanguage.injection 0 1 2) := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.mapsTo, OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.injection

theorem OAI.PartitionConsistency.ConcreteSystem.wellorderable_target_injection line 490
Source documentation
In the concrete system, surjections onto a wellorderable target admit sections densely. The common support is chosen before any fiber values.
```
theorem wellorderable_target_injection (f X Y : S.Name) (p : P)
    (hf : S.Forces ![f,X,Y] p (SetLanguage.surjection 0 1 2))
    (hY : S.Forces ![Y] p (SetLanguage.wellorderable 0)) :
    ∃ q, q ≤ p ∧ ∃ K : S.Name, S.Forces ![K,Y,X] q (SetLanguage.injection 0 1 2) := by
…
```
Mentions: OAI.PartitionConsistency.ConcreteSystem.P, OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.wellorderable, OAI.PartitionConsistency.ConcreteSystem.K, OAI.PartitionConsistency.SetLanguage.injection