Theorems · Theorem · general topology

MulAction.IsPretransitive.discreteTopology_iff

∀ {α : Type u_2} (G : Type u_4) [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] (x : α) [MulAction.IsPretransitive G α], DiscreteTopology α ↔ IsOpen {x}

Defined in

Mathlib.Topology.Algebra.ConstMulAction

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupMulActionContinuousConstSMulMulAction.IsPretransitive