Theorems · Theorem · manifolds

properVAdd_iff_continuousVAdd_ultrafilter_tendsto

∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X],
  ProperVAdd G X ↔
    ContinuousVAdd G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Filter.Tendsto (fun gx => (gx.1 +ᵥ gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) →
          ∃ g, g +ᵥ x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (nhds g)

An additive group G acts properly on a topological space X if and only if for all ultrafilters 𝒰 on X, if 𝒰 converges to (x₁, x₂) along the map (g, x) ↦ (g • x, x), then there exists g : G such that g • x₂ = x₁ and 𝒰.fst converges to g.

Defined in

Mathlib.Topology.Algebra.ProperAction.Basic

Cited by

0 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddActionTopologicalSpaceTopologicalSpace