Theorems · Theorem · Lie groups

Filter.neg_nhdsLT

∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousNeg H] {a : H}, -nhdsWithin a (Set.Iio a) = nhdsWithin (-a) (Set.Ioi (-a))

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommGroupPartialOrderIsOrderedAddMonoidContinuousNeg