SliceGeometry.lean`

40 declarations, 0 contain sorry, 0 declared as axioms

SubsetImage

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.defaultRelation_unique_on line 17

Source documentation

Local version of uniqueness for the default completion, using only the forced function property on its stated domain.

theorem defaultRelation_unique_on (f A B D d : S.Name) (p : P)
    (hf : S.Forces ![f,A,B] p (SetLanguage.mapsTo 0 1 2)) {q : P} (hq : q ≤ p)
    (a y z : S.Name) (ha : S.atomic.MemF q a A)
    (hy : (S.defaultRelation f D d).holds q a y) (hz : (S.defaultRelation f D d).holds q a z) :
    S.atomic.EqF q y z := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.mapsTo

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.subsetImageGraph line 34
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.subset_image_surjection line 49
Source documentation
Every single nonempty subset of a surjective image is itself a surjective image. The one default is explicitly given; no family of defaults is chosen.
```
theorem subset_image_surjection (f A B D d : S.Name) (p : P)
    (hf : S.Forces ![f,A,B] p (SetLanguage.surjection 0 1 2))
    (hD : S.SubsetF p D B) (hd : S.atomic.MemF p d D) :
    S.Forces ![S.subsetImageGraph f A D d,A,D] p (SetLanguage.surjection 0 1 2) := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.surjection
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.image line 80
Source documentation
Existential projection, with the regular forcing meaning of existence.
```
def image (R : S.BinaryRelation) : S.UnaryRelation where
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.image_move line 98
structure OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData line 110
Source documentation
Parameters of the ordinal slicing of a presentation and a surjection. There are no correctness assumptions in this structure.
```
structure SliceData (S : SymmetricSystem.{u} P Γ) where
…
```
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.support line 121
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.support_mem line 123
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.fix_s line 125
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.fix_f line 127
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.fix_A line 129
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.fix_X line 131
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.fix_Y line 133
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.slice line 136
Source documentation
The restriction of the presentation to the i-th Cartesian slice.
```
def slice (i : D.O) : S.BinaryRelation where
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.slice_move line 148
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.B line 156
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.fix_B line 160
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.mem_B line 163
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.B_subset line 174
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.occurrence line 179
Source documentation
An occurrence of a target value in f[B_i].
```
def occurrence (i : D.O) : S.UnaryRelation := (S.boundedApp D.f (D.B i) D.Y).image
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.occurrence_move line 181
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.Ypart line 188
Source documentation
The target pieces are occurrences at their least index in the fixed wellordering of the ground ordinal.
```
def Ypart (i : D.O) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.fix_Ypart line 193
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.mem_Ypart line 196
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.Ypart_subset line 201
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.Ypart_disjoint line 204
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.preimage line 209
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.preimage_move line 211
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.Spart line 217
Source documentation
The source pieces are B_i intersected with the preimages of Y_i.
```
def Spart (i : D.O) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.fix_Spart line 221
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.mem_Spart line 224
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.Spart_subset_B line 228
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.Spart_subset line 231
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.sliceGraph line 250
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.sliceGraph_surjection line 255
Source documentation
Each Cartesian slice surjects onto its actual image.
```
theorem sliceGraph_surjection (i : D.O) (p : P)
    (hs : S.Forces ![D.s,S.cartesianName D.A (Name.check D.O),D.X] p (SetLanguage.mapsTo 0 1 2)) :
    S.Forces ![D.sliceGraph i,D.A,D.B i] p (SetLanguage.surjection 0 1 2) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.mapsTo, OAI.PartitionConsistency.SetLanguage.surjection
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.partGraph line 275
Source documentation
Restrict f to the disjoint source and target pieces.
```
def partGraph (i : D.O) : S.Name := S.restrictionGraph D.f (D.Spart i) (D.Ypart i)
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.partGraph_surjection line 277

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.Spart_disjoint line 297

Source documentation

The source pieces need not cover X, but they are pairwise disjoint.

theorem Spart_disjoint (p : P)
    (hf : S.Forces ![D.f,D.X,D.Y] p (SetLanguage.mapsTo 0 1 2))
    {i j : D.O} {q : P} (hq : q ≤ p) {x : S.Name}
    (hi : S.atomic.MemF q x (D.Spart i)) (hj : S.atomic.MemF q x (D.Spart j)) : i = j := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.mapsTo

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.occurrence_cover line 310

Source documentation

All target values occur in some slice, densely with an actual ground index. No choice of slice indices is made.

theorem occurrence_cover (p : P)
    (hs : S.Forces ![D.s,S.cartesianName D.A (Name.check D.O),D.X] p (SetLanguage.surjection 0 1 2))
    (hf : S.Forces ![D.f,D.X,D.Y] p (SetLanguage.surjection 0 1 2))
    (y : S.Name) {q : P} (hq : q ≤ p) (hy : S.atomic.MemF q y D.Y) :
    ∀ r, r ≤ q → ∃ t, t ≤ r ∧ ∃ i : D.O, (D.occurrence i).holds t y := by
…

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

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.Ypart_cover line 335

Source documentation

Taking the least occurrence partitions the whole target.

theorem Ypart_cover (p : P)
    (hs : S.Forces ![D.s,S.cartesianName D.A (Name.check D.O),D.X] p (SetLanguage.surjection 0 1 2))
    (hf : S.Forces ![D.f,D.X,D.Y] p (SetLanguage.surjection 0 1 2))
    (y : S.Name) {q : P} (hq : q ≤ p) (hy : S.atomic.MemF q y D.Y) :
    ∀ r, r ≤ q → ∃ t, t ≤ r ∧ ∃ i : D.O, S.atomic.MemF t y (D.Ypart i) := by
…

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