PLRefinement.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Composition by a finite common subdivision

For h ∘ g, take every knot of g and the inverse image under g of every knot of h. Consecutive points of their sorted union lie in one piece of g and map into one piece of h. The two genuine affine equalities then compose, adding their integer slope exponents.

def OAI.ThompsonNonamenability.DyadicPLWitness.mul line 20
Source documentation
Composition of actual finite dyadic PL witnesses, using the sorted union of the inner breakpoints and pulled-back outer breakpoints.
```
noncomputable def mul {h g : IntervalHomeomorph}
    (wh : DyadicPLWitness h) (wg : DyadicPLWitness g)
    (_hhmono : StrictMono h) (hgmono : StrictMono g) : DyadicPLWitness (h * g) := by
…
```
Mentions: OAI.ThompsonNonamenability.IntervalHomeomorph, OAI.ThompsonNonamenability.DyadicPLWitness
theorem OAI.ThompsonNonamenability.HasDyadicPLPieces.mul line 105