Mathlib Map

Theorems · Theorem · Lie groups

nhds_mul_nhds_one

∀ {M : Type u_6} [inst : MulOneClass M] [inst_1 : TopologicalSpace M] [ContinuousMul M] (a : M),
  nhds a * nhds 1 = nhds a
Defined in
Mathlib.Topology.Algebra.Monoid
Cited by
2 results in Mathlib
Foundations
Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
MulOneClassTopologicalSpaceContinuousMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Filter.HasBasis.mul_self · cited by 0HasBasis.mul_selfnhds_mul · cited by 0nhds_mulTopologicalSpace · cited by 24529TopologicalSpaceFilter · cited by 8121Filternhds · cited by 5554nhdsmul_one · cited by 3885mul_oneMulOneClass · cited by 1018MulOneClassLE.le.antisymm · cited by 507le.antisymmContinuousMul · cited by 343ContinuousMulLE.le.trans_eq · cited by 328le.trans_eqpure_le_nhds · cited by 39pure_le_nhdsle_mul_of_one_le_right' · cited by 17le_mul_of_one_le_right'le_nhds_mul · cited by 2le_nhds_mulnhds_mul_nhds_oneCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.