CompactInvariantSets.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Minimal compact invariant subsets and their open covers.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_minimal_compact_invariant line 24

Source documentation

A nonempty compact invariant set contains a minimal nonempty closed invariant subset.

theorem exists_minimal_compact_invariant (T : G → A → A)
    (C : Set A) (hC : IsCompact C) (hne : C.Nonempty)
    (hinv : ∀ g, Set.MapsTo (T g) C C) :
    ∃ K : Set A, K ⊆ C ∧ K.Nonempty ∧ IsClosed K ∧
      (∀ g, Set.MapsTo (T g) K K) ∧
      ∀ L : Set A, L ⊆ K → L.Nonempty → IsClosed L →
        (∀ g, Set.MapsTo (T g) L L) → K ⊆ L := by
…

theorem OAI.BoundedHochschild.KadisonRingrose.minimal_invariant_open_cover line 61

Source documentation

Every orbit in a minimal compact invariant set meets each nonempty relatively open part of that set.

theorem minimal_invariant_open_cover (T : G → A → A)
    (hcont : ∀ g, Continuous (T g))
    (hone : ∀ x, T 1 x = x) (hmul : ∀ g h x, T (g * h) x = T g (T h x))
    (K : Set A) (hKc : IsClosed K) (hinv : ∀ g, Set.MapsTo (T g) K K)
    (hmin : ∀ L : Set A, L ⊆ K → L.Nonempty → IsClosed L →
      (∀ g, Set.MapsTo (T g) L L) → K ⊆ L)
    (U : Set A) (hU : IsOpen U) (hne : (K ∩ U).Nonempty) :
    K ⊆ ⋃ g, (T g) ⁻¹' U := by
…