BasicPartition.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Finite partitions into basic dyadic intervals

Closed cells cover the unit interval; their open interiors are disjoint. Restriction is the actual inverse image of the cell set under affine insertion.

structure OAI.ThompsonNonamenability.BasicPartition line 21
theorem OAI.ThompsonNonamenability.BasicPartition.ext line 30
def OAI.ThompsonNonamenability.BasicPartition.cellCount line 36
def OAI.ThompsonNonamenability.BasicPartition.Respects line 39
Source documentation
The interval is exactly covered by partition cells contained in it.
```
def Respects (T : BasicPartition) (I : BasicInterval) : Prop :=
…
```
Mentions: OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicPartition.cellCount_pos line 42
theorem OAI.ThompsonNonamenability.BasicPartition.respects_of_mem line 46
theorem OAI.ThompsonNonamenability.BasicPartition.interiors_overlap_of_mem_interior_mem_carrier line 51
theorem OAI.ThompsonNonamenability.BasicPartition.eq_of_mem_interior_mem_carrier line 65
Source documentation
At an interior point, even membership in another closed cell forces equality.
```
theorem eq_of_mem_interior_mem_carrier (T : BasicPartition)
    {I J : BasicInterval} (hI : I ∈ T.cells) (hJ : J ∈ T.cells)
    {x : ℝ} (hxI : x ∈ I.interior) (hxJ : x ∈ J.carrier) : I = J := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicPartition.respects_iff line 73
Source documentation
Equivalent geometric crossing condition, including the endpoint argument.
```
theorem respects_iff (T : BasicPartition) (I : BasicInterval) :
    T.Respects I ↔ ∀ K ∈ T.cells,
      (K.interior ∩ I.interior).Nonempty → K.Contained I := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicPartition.respects_of_mesh_lt line 108
Source documentation
A sufficiently fine actual partition respects the specified basic interval.
```
theorem respects_of_mesh_lt (T : BasicPartition) (I : BasicInterval)
    (hmesh : ∀ K ∈ T.cells, K.length < I.length) : T.Respects I := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.BasicInterval
def OAI.ThompsonNonamenability.BasicPartition.restrictCells line 120
Source documentation
Affinely normalized cells. Membership is exactly membership after insertion.
```
def restrictCells (T : BasicPartition) (I : BasicInterval) : Finset BasicInterval :=
…
```
Mentions: OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicPartition.mem_restrictCells line 124
def OAI.ThompsonNonamenability.BasicPartition.restrict line 129
Source documentation
The genuine partition obtained by restriction and affine normalization.
```
def restrict (T : BasicPartition) (I : BasicInterval) (h : T.Respects I) :
    BasicPartition where
…
```
Mentions: OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.BasicPartition.mem_restrict_cells line 153
theorem OAI.ThompsonNonamenability.BasicPartition.restrict_proof_irrel line 158
theorem OAI.ThompsonNonamenability.BasicPartition.restrict_cellCount_eq_filter_card line 162
theorem OAI.ThompsonNonamenability.BasicPartition.restrict_cellCount_lt line 173
theorem OAI.ThompsonNonamenability.BasicPartition.restrict_respects line 190
theorem OAI.ThompsonNonamenability.BasicPartition.restrict_restrict line 207