Theorems · Theorem · Lie groups

nonneg_nhds_iff

∀ {X : Type u_5} [inst : TopologicalSpace X] [T1Space X] [inst_2 : Zero X] {b : X}, 0 ≤ nhds b ↔ 0 = b

This lemma exists to ensure that we can still do the simplification pure_le_nhds_iff after simplifying with pure_zero.

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT1SpaceZero