Theorems · Theorem · Lie groups

Filter.map_divRight_nhdsGT

∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [IsTopologicalGroup H] [inst_3 : PartialOrder H]
  [IsOrderedMonoid H] {c a : H},
  Filter.map (fun x => x / c) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (a / c) (Set.Ioi (a / c))

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCommGroupIsTopologicalGroupPartialOrderIsOrderedMonoid