Theorems · Theorem · order theory
Filter.tendsto_abs_atTop_atTop
∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G], Filter.Tendsto abs Filter.atTop Filter.atTop$\lim_{x\to+\infty}|x|=+\infty$
- Defined in
- Mathlib.Order.Filter.AtTopBot.Group
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Quot.sound
- Assumes
- AddCommGroupLinearOrder
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.
- AddCommGroupstatement and proof · cited by 12,871
- LinearOrderstatement and proof · cited by 8,572
- Filter.Tendstostatement · cited by 3,814
- Filter.atTopstatement · cited by 2,405
- absstatement · cited by 1,814
- Filter.tendsto_idproof · cited by 180
- le_abs_selfproof · cited by 113
- Filter.tendsto_atTop_monoproof · cited by 22
Cited by9
Results whose statement or proof uses this declaration.
- tendsto_norm_atTop_atTopproof · cited by 6
- Polynomial.abs_tendsto_atTopproof · cited by 3
- tendsto_intCast_atBot_sup_atTop_coboundedproof · cited by 2
- Filter.comap_abs_atTopproof · cited by 2
- RCLike.tendsto_ofReal_atTop_coboundedproof · cited by 2
- Polynomial.abs_div_tendsto_atTop_atTop_of_degree_gtproof · cited by 2
- Complex.IsExpCmpFilter.tendsto_abs_reproof · cited by 2
- Asymptotics.isLittleO_const_id_atTopproof · cited by 0
- Real.one_isLittleO_log_logproof · cited by 0