Theorems · Theorem · general topology

AddAction.IsPretransitive.t1Space_iff

∀ {α : Type u_2} (G : Type u_4) [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] (x : α) [AddAction.IsPretransitive G α], T1Space α ↔ IsClosed {x}

Defined in

Mathlib.Topology.Algebra.ConstMulAction

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddGroupAddActionContinuousConstVAddAddAction.IsPretransitive