Theorems · Theorem · Lie groups
Continuous.abs
∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
[OrderTopology G] {X : Type u_2} [inst_5 : TopologicalSpace X] {f : X → G}, Continuous f → Continuous fun x => |f x|- Defined in
- Mathlib.Topology.Algebra.Order.Group
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- AddCommGroupstatement and proof · cited by 12,871
- LinearOrderstatement and proof · cited by 8,572
- Continuousstatement and proof · cited by 2,592
- absstatement · cited by 1,814
- IsOrderedAddMonoidstatement and proof · cited by 1,659
- OrderTopologystatement and proof · cited by 1,355
- Continuous.compproof · cited by 371
- continuous_absproof · cited by 13
Cited by12
Results whose statement or proof uses this declaration.
- ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mulproof · cited by 3
- ContinuousMap.abs_mem_subalgebra_closureproof · cited by 2
- Complex.continuousAt_cpow_zero_of_re_posproof · cited by 2
- ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mulproof · cited by 2
- ProbabilityTheory.integrable_exp_mul_abs_addproof · cited by 2
- MeasureTheory.measureReal_abs_gt_le_integral_charFunproof · cited by 2
- ModularGroup.isClosed_fdproof · cited by 1
- ModularGroup.isOpen_fdoproof · cited by 1
- ODE.FunSpace.dist_iterate_next_apply_leproof · cited by 1
- MeasureTheory.measureReal_abs_inner_gt_le_integral_charFunproof · cited by 1
- MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDualproof · cited by 0