Theorems · Theorem · Lie groups

IsClosed.right_addCoset

∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {U : Set G},
  IsClosed U → ∀ (x : G), IsClosed (AddOpposite.op x +ᵥ U)

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddGroupSeparatelyContinuousAdd