HyperspaceIncidence.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Closed continuum incidences in compact level graphs

The compatibility condition quantifies over subcontinua of a finite level union. The hyperspace of nonempty compact sets is compact, and connectedness, point membership and containment in a closed level graph are closed conditions. Projection therefore preserves closedness for continuum incidences with a fixed positive size witness.

theorem OAI.CircleDomainRigidity.isClosed_connected_nonemptyCompacts line 24
theorem OAI.CircleDomainRigidity.isClosed_nonemptyCompacts_membership line 52
theorem OAI.CircleDomainRigidity.isClosed_compact_subset_graph line 61
def OAI.CircleDomainRigidity.positiveContinuumIncidence line 84
theorem OAI.CircleDomainRigidity.isClosed_positiveContinuumIncidence line 92
Source documentation
The compact hyperspace witnesses make each positive-size continuum incidence a closed relation in the point and level parameters.
```
theorem isClosed_positiveContinuumIncidence
    {X T : Type*} [MetricSpace X] [CompactSpace X] [TopologicalSpace T]
    {R : Set (X × T)} (hR : IsClosed R) (ε : ℝ) :
    IsClosed (positiveContinuumIncidence R ε) := by
…
```
Mentions: OAI.CircleDomainRigidity.positiveContinuumIncidence
def OAI.CircleDomainRigidity.nontrivialFiberComponentRelation line 123
theorem OAI.CircleDomainRigidity.isClosed_connectedComponentIn_of_isClosed line 127
theorem OAI.CircleDomainRigidity.nontrivialFiberComponentRelation_eq_iUnion line 136

theorem OAI.CircleDomainRigidity.measurableSet_nontrivialFiberComponentRelation line 171

Source documentation

The relation “the point belongs to a nondegenerate component of the compact level fiber” is Fσ, hence Borel.

theorem measurableSet_nontrivialFiberComponentRelation
    {X T : Type*} [MetricSpace X] [CompactSpace X] [TopologicalSpace T]
    [MeasurableSpace (X × T)] [BorelSpace (X × T)]
    {R : Set (X × T)} (hR : IsClosed R) :
    MeasurableSet (nontrivialFiberComponentRelation R) := by
…

Mentions: OAI.CircleDomainRigidity.nontrivialFiberComponentRelation