Theorems · Theorem · Lie groups

one_le_nhds_iff

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

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

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

TopologicalSpaceT1SpaceOne