OAI/Analysis/FiniteFactor/OrbitSampling/CylinderBasis.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.rational_Icc_nhds line 10
2. theorem OAI.FiniteFactor.sourceSamplingCylinder_basis line 19

   Source documentation

   The finite rational cylinders contain arbitrarily small neighborhoods in the full real product, including points outside the unit cube.

   theorem sourceSamplingCylinder_basis (u : Set SourceSamplingPair) (hu : IsOpen u)
       (p : SourceSamplingPair) (hp : p ∈ u) :
       ∃ s ∈ Set.range sourceSamplingCylinder, s ∈ 𝓝 p ∧ s ⊆ u := by
   …

   Mentions: OAI.FiniteFactor.SourceSamplingPair, OAI.FiniteFactor.sourceSamplingCylinder