SymmetricSets.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.codeOrder line 12
Source documentation
The ordering on literal condition codes, false outside those codes.
```
def codeOrder (a b : ZFSet.{u}) : Prop :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.codeOrder_codes line 15
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.codeOrder_symmetry line 23
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.union line 36
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.edge_union line 42
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_union line 59
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_union line 81
Source documentation
The Union axiom for arbitrary HS input names.
```
theorem forces_union (p : P) : S.Forces Fin.elim0 p SetLanguage.union := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.union
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.code_top_fixed line 98
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.pair line 104
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check line 108
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check_raw line 112
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check_empty line 114
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.edge_pair line 122
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_pair line 129
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_pairing line 145
Source documentation
The Pairing axiom, with the standard largest-condition name.
```
theorem forces_pairing (p : P) : S.Forces Fin.elim0 p SetLanguage.pairing := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.pairing
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_check line 156
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.check_mem_of_mem line 171

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.check_successor line 176

Source documentation

The check name of a ground successor is its internal successor.

theorem check_successor (x : ZFSet.{u}) (ν : S.Name) (p : P) :
    S.atomic.MemF p ν (Name.check (insert x x)) ↔
      ∀ q, q ≤ p → ∃ r, r ≤ q ∧
        (S.atomic.MemF r ν (Name.check x) ∨ S.atomic.EqF r ν (Name.check x)) := by
…

Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_infinity line 196
Source documentation
The Infinity witness is the literal check-name of the ground natural numbers.
```
theorem forces_infinity (p : P) : S.Forces Fin.elim0 p SetLanguage.infinity := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.infinity

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.collectName_fixed line 242

Source documentation

The same entry-permutation argument records the particular fixing subgroup, not merely that some subgroup in the filter fixes the collected name.

theorem collectName_fixed {ι : Type t} [Small.{u} ι] (f : ι → S.Name) (R : ι → P → Prop)
    (H : Subgroup Γ)
    (permutes : ∀ g ∈ H, ∀ i p, R i p → ∃ j,
      f j = g • f i ∧ R j (S.move g p)) (g : Γ) (hg : g ∈ H) :
    g • S.collectName f R = S.collectName f R := by
…

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SubsetF line 262
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_subset line 265
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.subset_mono line 272
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.subset_of_dense line 275
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.subset_congr line 283
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.subset_symmetry line 294
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.subsetBound line 301
Source documentation
All possible immediate pairs over the domain of a particular name form a set. This is a bound on normalizations of subsets, not on all HS names.
```
noncomputable def subsetBound (σ : S.Name) : ZFSet.{u} :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.subsetBound_fixed line 304
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.PowerCandidate line 319
Source documentation
The actual HS candidates inside the small set of normalization codes.
```
def PowerCandidate (σ : S.Name) := {ν : S.Name // ν.raw ⊆ S.subsetBound σ}
```
instance OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.(instance at line 321) line 321
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.normalize line 327
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_normalize line 330
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.normalize_bounded line 334
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.normalize_eq line 341
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.powerCandidate_permute line 348
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.power line 363
Source documentation
The power-set name uses every HS normalized subset candidate and the conditions which force that candidate to be a subset.
```
noncomputable def power (σ : S.Name) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.edge_power line 367
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_power line 381
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_powerSet line 400
Source documentation
Power Set with quantification over every HS name, including subsets at arbitrarily high name ranks.
```
theorem forces_powerSet (p : P) : S.Forces Fin.elim0 p SetLanguage.powerSet := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.powerSet