UniformImages.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

KernelImage

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.kernelRelation line 16
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.kernelRelation_move line 19
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.kernelGraph line 29
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.kernelGraph_fixed line 36
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.app_kernelGraph line 44

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.app_kernelGraph_value line 61

Source documentation

Kernel membership says exactly equality of the actual function values; no representatives of classes have been chosen.

theorem app_kernelGraph_value {h A B a y : S.Name} {p q : P}
    (hf : S.Forces ![h,A,B] p (SetLanguage.mapsTo 0 1 2)) (hq : q ≤ p)
    (ha : S.atomic.MemF q a A) (hay : S.App q h a y) (b : S.Name) :
    S.App q (S.kernelGraph h A B) a b ↔ S.atomic.MemF q b A ∧ S.App q h b y := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.mapsTo

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.kernel_class_same_value line 80
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.imageClassRelation line 93
Source documentation
Graph of the representative-free correspondence h(a) ↦ [a].
```
def imageClassRelation (h A B : S.Name) : S.BinaryRelation where
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.imageClassRelation_move line 118
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.imageClassRelation_one line 130
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.imageClassRelation_inj line 145
abbrev OAI.PartitionConsistency.ConcreteSystem.A line 175
def OAI.PartitionConsistency.ConcreteSystem.imageQuotient line 177
theorem OAI.PartitionConsistency.ConcreteSystem.mem_imageQuotient line 180
def OAI.PartitionConsistency.ConcreteSystem.imageQuotientGraph line 188
theorem OAI.PartitionConsistency.ConcreteSystem.app_imageQuotientGraph line 197
theorem OAI.PartitionConsistency.ConcreteSystem.imageQuotientGraph_mapsTo line 203
theorem OAI.PartitionConsistency.ConcreteSystem.imageQuotientGraph_injection line 216
theorem OAI.PartitionConsistency.ConcreteSystem.imageQuotientGraph_surjection line 227
theorem OAI.PartitionConsistency.ConcreteSystem.nonwellorderable_image_bijection line 243
Source documentation
Every nonwellorderable image of A is now bijective to A. This is obtained from the actual kernel quotient and its representative-free graph.
```
theorem nonwellorderable_image_bijection (h B : S.Name) (p : P)
    (hf : S.Forces ![h,A,B] p (SetLanguage.surjection 0 1 2))
    (hno : S.Forces ![B] p (SetLanguage.wellorderable 0).neg) :
    ∃ q, q ≤ p ∧ ∃ f : S.Name,
      S.Forces ![f,A,B] q ((SetLanguage.surjection 0 1 2).conj (SetLanguage.injection 0 1 2)) := by
…
```
Mentions: OAI.PartitionConsistency.ConcreteSystem.P, OAI.PartitionConsistency.ConcreteSystem.A, OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.wellorderable, OAI.PartitionConsistency.SetLanguage.injection

theorem OAI.PartitionConsistency.ConcreteSystem.uniform_maximum_dense line 291

Source documentation

Simultaneous use of the localized maximum principle. The same larger root is chosen before any witnesses, hence all the witnesses have one common support, even for a ground family of arbitrarily large small cardinality.

theorem uniform_maximum_dense {ι : Sort*} {n} (φ : Formula (n+1))
    (v : ι → Fin n → S.Name) (H : Subgroup (Equiv.Perm I)) (hH : H ∈ S.filter)
    (hv : ∀ g ∈ H, ∀ i k, g • v i k = v i k)
    (t : P) (hf : ∀ i, S.Forces (v i) t φ.ex) :
    ∃ r, r ≤ t ∧ ∃ G : Subgroup (Equiv.Perm I), G ∈ S.filter ∧
      ∃ f : ι → S.Name, (∀ g ∈ G, ∀ i, g • f i = f i) ∧
        ∀ i, S.Forces (Fin.snoc (v i) (f i)) r φ := by
…

Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.ConcreteSystem.I, OAI.PartitionConsistency.ConcreteSystem.P