CohenForcing.lean`

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.PartitionConsistency.CohenForcing.Condition line 13
Source documentation
Countable partial functions I × κ → 2, represented by their graphs. Countability of the graph is equivalent to countability of the domain for these single-valued graphs. Conditions are ordered by reverse inclusion.
```
structure Condition (I : Type u) (κ : Type v) where
…
```
theorem OAI.PartitionConsistency.CohenForcing.Condition.ext line 20
instance OAI.PartitionConsistency.CohenForcing.Condition.(instance at line 23) line 23
theorem OAI.PartitionConsistency.CohenForcing.Condition.le_iff line 29
instance OAI.PartitionConsistency.CohenForcing.Condition.(instance at line 31) line 31
theorem OAI.PartitionConsistency.CohenForcing.Condition.graph_top line 35
def OAI.PartitionConsistency.CohenForcing.Condition.dom line 37
def OAI.PartitionConsistency.CohenForcing.Condition.support line 38
theorem OAI.PartitionConsistency.CohenForcing.Condition.countable_dom line 40
theorem OAI.PartitionConsistency.CohenForcing.Condition.countable_support line 43
theorem OAI.PartitionConsistency.CohenForcing.Condition.mem_dom line 46
theorem OAI.PartitionConsistency.CohenForcing.Condition.mem_support line 54
theorem OAI.PartitionConsistency.CohenForcing.Condition.countable_graph_iff_dom line 64
Source documentation
The graph description is equivalent to the source's countable-domain condition for partial functions, and does not impose an extra smallness bound.
```
theorem countable_graph_iff_dom {g : Set ((I × κ) × Bool)}
    (hg : ∀ a b c, (a, b) ∈ g → (a, c) ∈ g → b = c) :
    g.Countable ↔ (Prod.fst '' g).Countable := by
…
```
def OAI.PartitionConsistency.CohenForcing.Condition.Compatible line 75
Source documentation
Compatibility is exactly agreement wherever both assignments are defined.
```
def Compatible (p q : Condition I κ) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.CohenForcing.Condition.Compatible.symm line 78
def OAI.PartitionConsistency.CohenForcing.Condition.union line 81
theorem OAI.PartitionConsistency.CohenForcing.Condition.union_graph line 92
theorem OAI.PartitionConsistency.CohenForcing.Condition.union_le_left line 95
theorem OAI.PartitionConsistency.CohenForcing.Condition.union_le_right line 98
theorem OAI.PartitionConsistency.CohenForcing.Condition.compatible_iff line 101
theorem OAI.PartitionConsistency.CohenForcing.Condition.countably_closed line 111
Source documentation
The Cohen forcing described in the source is countably closed. Unions suffice; no closure of the diagram forcing or product is asserted.
```
theorem countably_closed (p : ℕ → Condition I κ) (hp : Antitone p) :
    ∃ r : Condition I κ, ∀ n, r ≤ p n := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
def OAI.PartitionConsistency.CohenForcing.Condition.restrict line 124
Source documentation
Restriction to a set of label coordinates.
```
def restrict (p : Condition I κ) (J : Set I) : Condition I κ where
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.CohenForcing.Condition.mem_restrict line 129
theorem OAI.PartitionConsistency.CohenForcing.Condition.le_restrict line 132
theorem OAI.PartitionConsistency.CohenForcing.Condition.support_restrict_subset line 135
theorem OAI.PartitionConsistency.CohenForcing.Condition.restrict_eq_of_support_subset line 141
def OAI.PartitionConsistency.CohenForcing.Condition.coordinatePerm line 151
Source documentation
Define the coordinate action on the full graph, including both the ordinal input and its Boolean output.
```
def coordinatePerm (π : Equiv.Perm I) : Equiv.Perm ((I × κ) × Bool) :=
…
```
theorem OAI.PartitionConsistency.CohenForcing.Condition.coordinatePerm_apply line 154
theorem OAI.PartitionConsistency.CohenForcing.Condition.coordinatePerm_symm_apply line 156
def OAI.PartitionConsistency.CohenForcing.Condition.permute line 159
theorem OAI.PartitionConsistency.CohenForcing.Condition.mem_permute line 166
theorem OAI.PartitionConsistency.CohenForcing.Condition.permute_one line 170
theorem OAI.PartitionConsistency.CohenForcing.Condition.permute_mul line 174
theorem OAI.PartitionConsistency.CohenForcing.Condition.permute_inv_permute line 180
theorem OAI.PartitionConsistency.CohenForcing.Condition.permute_permute_inv line 186
def OAI.PartitionConsistency.CohenForcing.Condition.permuteOrderIso line 194
Source documentation
The same label permutations used for diagrams are order automorphisms of Cohen forcing. They can therefore act diagonally on the product.
```
def permuteOrderIso (π : Equiv.Perm I) : Condition I κ ≃o Condition I κ where
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.CohenForcing.Condition.permute_eq_of_fixes_support line 204
theorem OAI.PartitionConsistency.CohenForcing.Condition.compatible_of_disjoint_off_root line 218
Source documentation
Two conditions agreeing on their common root and having disjoint nonroot supports are compatible. This is the Cohen half of the locality argument.
```
theorem compatible_of_disjoint_off_root (p q : Condition I κ) (J : Set I)
    (hroot : Compatible (restrict p J) (restrict q J))
    (hdisj : Disjoint (p.support \ J) (q.support \ J)) : Compatible p q := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.CohenForcing.Condition.Compatible, OAI.PartitionConsistency.CohenForcing.Condition.restrict
def OAI.PartitionConsistency.CohenForcing.Condition.insert line 229
Source documentation
Introduce one unassigned coordinate with a specified Boolean value.
```
def insert (p : Condition I κ) (a : I × κ) (b : Bool) (h : a ∉ p.dom) : Condition I κ where
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.CohenForcing.Condition.insert_le line 242
theorem OAI.PartitionConsistency.CohenForcing.Condition.fresh_level line 245
theorem OAI.PartitionConsistency.CohenForcing.Condition.separate_labels line 256
Source documentation
Distinct label coordinates can be assigned opposite bits at a fresh level below every condition. This is the dense separation used for distinct labels.
```
theorem separate_labels [Uncountable κ] (p : Condition I κ) {j k : I} (hjk : j ≠ k) :
    ∃ (q : Condition I κ) (a : κ), q ≤ p ∧
      ((j, a), false) ∈ q.graph ∧ ((k, a), true) ∈ q.graph := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition