Theorems · Definition · dynamical systems

MulAction.IsTopologicallyTransitive.casesOn

{M : Type u_1} →
  {α : Type u_2} →
    [inst : Monoid M] →
      [inst_1 : TopologicalSpace α] →
        [inst_2 : MulAction M α] →
          {motive : MulAction.IsTopologicallyTransitive M α → Sort u} →
            (t : MulAction.IsTopologicallyTransitive M α) →
              ((exists_smul_inter :
                    ∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ m, (m • U ∩ V).Nonempty) →
                  motive ⋯) →
                motive t

Defined in

Mathlib.Dynamics.Transitive

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

MonoidTopologicalSpaceMulAction