PlacementExtensions.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PartitionConsistency.SmallPlacements.countable_obstructions line 13
Source documentation
Only countably many members of a pairwise disjoint family meet a fixed countable set. This will be applied to the nonroot supports of probe copies.
```
theorem countable_obstructions {I A : Type*} (S : A → Set I) (C : Set I)
    (hS : Pairwise (fun a b => Disjoint (S a) (S b))) (hC : C.Countable) :
    {a | (S a ∩ C).Nonempty}.Countable :=
…
```
theorem OAI.PartitionConsistency.SmallPlacements.exists_fresh_member line 22
Source documentation
An uncountable family of disjoint nonroot supports always has a member avoiding any specified countable collection of coordinates.
```
theorem exists_fresh_member {I A : Type*} [Uncountable A] (S : A → Set I)
    (C : Set I) (hS : Pairwise (fun a b => Disjoint (S a) (S b))) (hC : C.Countable) :
    ∃ a, Disjoint (S a) C := by
…
```
theorem OAI.PartitionConsistency.CohenForcing.Condition.Compatible.refl line 38
theorem OAI.PartitionConsistency.CohenForcing.Condition.Compatible.weaken line 42
Source documentation
Weakening either of two compatible partial functions preserves their compatibility. Recall that the forcing order is reverse inclusion.
```
theorem Compatible.weaken {p q p' q' : Condition I κ} (h : Compatible p q)
    (hp : p ≤ p') (hq : q ≤ q') : Compatible p' q' :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.CohenForcing.Condition.Compatible
theorem OAI.PartitionConsistency.CohenForcing.Condition.Compatible.of_le line 46
def OAI.PartitionConsistency.CohenForcing.Condition.probeDenseSet line 52
Source documentation
The explicit ground dense set in the probe argument for ordinal choice (source equation eq:probe-cohen-dense). It contains conditions incompatible with the common root and conditions extending one of the placed copies.
```
def probeDenseSet (root : Condition I κ) (copies : A → Condition I κ) :
    Set (Condition I κ) :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.CohenForcing.Condition.probeDenseSet_dense line 59
Source documentation
Pairwise independent copies with the same Cohen root give the probe dense set. Uncountability is sufficient: a test condition has countable support. No forcing name, generic extension, or choice in a symmetric model is assumed.
```
theorem probeDenseSet_dense [Uncountable A] (J : Set I) (root : Condition I κ)
    (copies : A → Condition I κ) (hroot : ∀ a, (copies a).restrict J = root)
    (hdisj : Pairwise (fun a b => Disjoint ((copies a).support \ J) ((copies b).support \ J))) :
    ForcingQuotient.Dense (probeDenseSet root copies) := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.CohenForcing.Condition.restrict, OAI.PartitionConsistency.CohenForcing.Condition.support, OAI.PartitionConsistency.ForcingQuotient.Dense, OAI.PartitionConsistency.CohenForcing.Condition.probeDenseSet
theorem OAI.PartitionConsistency.CohenForcing.Condition.meets_probe line 80
Source documentation
A filter containing the common root and meeting the displayed dense set contains an extension of one of the copies. It is not necessary, and would be incorrect, to assume that any preselected moved condition belongs to the filter.
```
theorem meets_probe {root : Condition I κ} {copies : A → Condition I κ}
    (G : ForcingQuotient.GenericFilter (Condition I κ)) (hroot : root ∈ G)
    (hmeets : ∃ c : Condition I κ, c ∈ G ∧ c ∈ probeDenseSet root copies) :
    ∃ a, ∃ c : Condition I κ, c ∈ G ∧ c ≤ copies a := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ForcingQuotient.GenericFilter, OAI.PartitionConsistency.CohenForcing.Condition.probeDenseSet