StandardCharacterization.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Identification with the standard finite-breakpoint PL definition

The standard condition below states only a finite strictly ordered list of dyadic knots, the two endpoints, and the powers-of-two affine formulas. Coverage is derived from the endpoints; it is not an additional premise.

def OAI.ThompsonNonamenability.StandardPLCondition line 17
Source documentation
The usual increasing PL interval homeomorphisms with finitely many dyadic breakpoints and slopes in the integer powers of two.
```
def StandardPLCondition (f : UnitInterval ≃ₜ UnitInterval) : Prop :=
…
```
Mentions: OAI.ThompsonNonamenability.UnitInterval
theorem OAI.ThompsonNonamenability.intervalHomeomorph_standardPL_iff line 30
theorem OAI.ThompsonNonamenability.F.standardPLCondition line 52
def OAI.ThompsonNonamenability.F.standardPLEquiv line 57
Source documentation
A faithful identification with the standard PL group carrier, with no uniform-grid or transport assumption in the right-hand side.
```
def standardPLEquiv : F ≃ {f : UnitInterval ≃ₜ UnitInterval // StandardPLCondition f} where
…
```
Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.UnitInterval, OAI.ThompsonNonamenability.StandardPLCondition
theorem OAI.ThompsonNonamenability.F.standardPLEquiv_apply line 68