SliceAssembly.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

SliceAssembly

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.falseRelation line 16
Source documentation
The empty binary relation, with its regular interpretation.
```
def falseRelation : S.BinaryRelation where
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.empty_domain_injection line 23
Source documentation
An empty domain has an internal injection into any set.
```
theorem empty_domain_injection (X Y : S.Name) (p : P)
    (hX : ∀ x q, q ≤ p → ¬ S.atomic.MemF q x X) :
    ∃ j : S.Name, S.Forces ![j,X,Y] p (SetLanguage.injection 0 1 2) := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.injection
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.empty_domain_wellorderable line 38
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.nonwellorderable_member_dense line 46
Source documentation
Nonwellorderability alone supplies a member densely. This selects only one member below one condition, never a family of default members.
```
theorem nonwellorderable_member_dense (X : S.Name) (p : P)
    (hX : S.Forces ![X] p (SetLanguage.wellorderable 0).neg) :
    ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ x : S.Name, S.atomic.MemF r x X := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.wellorderable
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SliceData.assemble line 61
Source documentation
A uniformly supported family of candidate injections is assembled into one graph. Totality uses the target partition, while one-to-one-ness uses the disjoint source pieces. No assertion that these source pieces cover X is made.
```
theorem assemble (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))
    (c : D.O → S.Name) (H : Subgroup Γ) (hH : H ∈ S.filter) (hHD : H ≤ D.support)
    (hc : ∀ g ∈ H, ∀ i, g • c i = c i)
    (hj : ∀ i, S.Forces ![c i,D.Ypart i,D.Spart i] p (SetLanguage.injection 0 1 2)) :
    ∃ j : S.Name, S.Forces ![j,D.Y,D.X] p (SetLanguage.injection 0 1 2) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.injection
theorem OAI.PartitionConsistency.ConcreteSystem.slice_candidate line 118
Source documentation
Pointwise existence of a candidate. The wellorderable case uses ordinal choice for the fibers of this one slice. In the other case two classified images of A give a reverse injection; it need not be a section of f.
```
theorem slice_candidate (D : SliceData S) (hA : D.A = A) (i : D.O) (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)) :
    ∃ q, q ≤ p ∧ ∃ j : S.Name,
      S.Forces ![j,D.Ypart i,D.Spart i] q (SetLanguage.injection 0 1 2) := by
…
```
Mentions: OAI.PartitionConsistency.ConcreteSystem.S, OAI.PartitionConsistency.ConcreteSystem.A, OAI.PartitionConsistency.ConcreteSystem.P, OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.injection
theorem OAI.PartitionConsistency.ConcreteSystem.presentation_reverse_injection line 161
Source documentation
Choose the already defined slice injections with one common support and assemble them. There is no simultaneous selection of auxiliary wellorderings, defaults, or quotient bijections in the pointwise argument.
```
theorem presentation_reverse_injection (D : SliceData S) (hA : D.A = A) (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)) :
    ∃ q, q ≤ p ∧ ∃ j : S.Name, S.Forces ![j,D.Y,D.X] q (SetLanguage.injection 0 1 2) := by
…
```
Mentions: OAI.PartitionConsistency.ConcreteSystem.S, OAI.PartitionConsistency.ConcreteSystem.A, OAI.PartitionConsistency.ConcreteSystem.P, OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.injection