ProductForcing.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PartitionConsistency.SmallPlacements.union_bound line 14

theorem OAI.PartitionConsistency.SmallPlacements.intersection_eq_root line 20

Source documentation

An independent placement has exactly the stated common root.

theorem intersection_eq_root {s t r : Set I} (hrs : r ⊆ s) (hrt : r ⊆ t)
    (π : Equiv.Perm I) (hfix : ∀ x ∈ r, π x = x)
    (hdisj : Disjoint (π '' (s \ r)) (t ∪ r)) : t ∩ π '' s = r := by
…

theorem OAI.PartitionConsistency.DiagramForcing.Diagram.range_permute line 37
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.cardinal_range line 43
Source documentation
Diagram ranges have exactly the cardinality of the monoid.
```
@[simp] theorem cardinal_range (s : Diagram M I) : Cardinal.mk s.range = Cardinal.mk M :=
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.permute_eq_of_fixes_range line 46
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.ExactOverlap.symm line 53
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.common_extension_two line 59
Source documentation
The binary specialization of finite diagram amalgamation.
```
theorem common_extension_two [Infinite I] [DiagramOrder.IsConical M]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    {r s : Diagram M I} (hov : ExactOverlap r s) :
    ∃ t : Diagram M I, t ≤ r ∧ t ≤ s := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.IsConical, OAI.PartitionConsistency.DiagramForcing.HasFiniteMergers, OAI.PartitionConsistency.DiagramForcing.Diagram, OAI.PartitionConsistency.DiagramForcing.Diagram.ExactOverlap
theorem OAI.PartitionConsistency.CohenForcing.Condition.support_permute line 78
theorem OAI.PartitionConsistency.CohenForcing.Condition.cardinal_support line 90
theorem OAI.PartitionConsistency.CohenForcing.Condition.restrict_permute_of_fixes line 94
Source documentation
Fixing the root preserves the Cohen restriction literally.
```
theorem restrict_permute_of_fixes (π : Equiv.Perm I) (p : Condition I κ)
    {J : Set I} (hfix : ∀ j ∈ J, π j = j) :
    restrict (permute π p) J = restrict p J := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.CohenForcing.Condition.restrict, OAI.PartitionConsistency.CohenForcing.Condition.permute
abbrev OAI.PartitionConsistency.ProductForcing.Condition line 118
Source documentation
The actual product of the Cohen and ground diagram posets.
```
abbrev Condition (M I : Type u) (κ : Type v) :=
…
```
def OAI.PartitionConsistency.ProductForcing.permute line 122
Source documentation
Simultaneous transport of labels in both coordinates, as in the paper.
```
def permute (π : Equiv.Perm I) (p : Condition M I κ) : Condition M I κ :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Condition
theorem OAI.PartitionConsistency.ProductForcing.permute_one line 125
theorem OAI.PartitionConsistency.ProductForcing.permute_mul line 128
def OAI.PartitionConsistency.ProductForcing.permuteOrderIso line 134
theorem OAI.PartitionConsistency.ProductForcing.compatible_placement line 149
Source documentation
The independent-placement step of local decision (source lem:local-decision). Compatible root restrictions suffice to place the second product condition compatibly with the first, fixing the entire root diagram. The monoid finite-merger property remains an explicit, unconstructed input.
```
theorem compatible_placement [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (p s₀ s₁ : Diagram M I) (hs₀ : s₀ ≤ p) (hs₁ : s₁ ≤ p)
    (d₀ d₁ : CohenForcing.Condition I κ)
    (hroot : CohenForcing.Condition.Compatible (d₀.restrict p.range) (d₁.restrict p.range)) :
    ∃ π : Equiv.Perm I, (∀ j ∈ p.range, π j = j) ∧
      s₀.range ∩ (s₁.permute π).range = p.range ∧
      ∃ q : Condition M I κ, q ≤ (d₀, s₀) ∧ q ≤ permute π (d₁, s₁) := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.CohenForcing.Condition.Compatible, OAI.PartitionConsistency.ProductForcing.Condition, OAI.PartitionConsistency.ProductForcing.permute