Theorems · Theorem · Lie groups
ContinuousAt.fun_sub
∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Sub G]
[ContinuousSub G] {f g : X → G} {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun i => f i - g i) xEta-expanded form of ContinuousAt.sub
- Defined in
- Mathlib.Topology.Algebra.Group.Defs
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- ContinuousAtstatement · cited by 697
- ContinuousSubstatement · cited by 48
- ContinuousAt.subproof · cited by 9
Cited by19
Results whose statement or proof uses this declaration.
- tendsto_zero_of_meromorphicOrderAt_posproof · cited by 4
- mapClusterPt_self_zsmul_atTop_nsmulproof · cited by 3
- ConvexOn.continuousOn_tfaeproof · cited by 3
- tendsto_cobounded_of_meromorphicOrderAt_negproof · cited by 3
- natCast_le_analyticOrderAtproof · cited by 2
- ZetaAsymptotics.term_welldefproof · cited by 2
- OpenPartialHomeomorph.hasFPowerSeriesAt_symmproof · cited by 2
- MeromorphicAt.analyticAtproof · cited by 2
- BddAbove.continuous_convolution_right_of_integrableproof · cited by 2
- Subalgebra.frontier_spectrumproof · cited by 2
- closure_subset_add_self_of_mem_nhds_zeroproof · cited by 2
- MeromorphicAt.eventually_continuousAtproof · cited by 1