Theorems · Definition · dynamical systems

AddAction.IsTopologicallyTransitive.casesOn

{M : Type u_1} →
  {α : Type u_2} →
    [inst : AddMonoid M] →
      [inst_1 : TopologicalSpace α] →
        [inst_2 : AddAction M α] →
          {motive : AddAction.IsTopologicallyTransitive M α → Sort u} →
            (t : AddAction.IsTopologicallyTransitive M α) →
              ((exists_vadd_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

AddMonoidTopologicalSpaceAddAction