Theorems · Theorem · Lie groups
map_add_left_nhds_zero
∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (x : G),
Filter.map (fun x_1 => x + x_1) (nhds 0) = nhds x- Defined in
- Mathlib.Topology.Algebra.Group.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- AddGroupstatement and proof · cited by 4,410
- add_zeroproof · cited by 2,707
- IsTopologicalAddGroupstatement and proof · cited by 1,394
- Filter.mapstatement · cited by 819
- map_add_left_nhdsproof · cited by 3
Cited by13
Results whose statement or proof uses this declaration.
- IsBoundedBilinearMap.hasStrictFDerivAtproof · cited by 7
- hasFDerivAt_iff_isLittleO_nhds_zeroproof · cited by 7
- HasFDerivAt.le_of_lip'proof · cited by 4
- LocallyConvexSpace.ofBasisZeroproof · cited by 3
- continuousAt_gaugeproof · cited by 2
- WithSeminorms.hasBasis_ballproof · cited by 2
- Ideal.hasBasis_nhds_adicproof · cited by 2
- continuous_of_tendsto_nhds_zeroproof · cited by 2
- continuous_of_continuousAt_zero₂proof · cited by 1
- one_mem_posTangentConeAt_iff_mem_closureproof · cited by 1
- hasFPowerSeriesAt_iff'proof · cited by 0
- IsTopologicalAddGroup.isOpenMap_iff_nhds_zeroproof · cited by 0