Theorems · Theorem · general topology
Continuous.div_const
∀ {α : Type u_1} {G₀ : Type u_3} [inst : DivInvMonoid G₀] [inst_1 : TopologicalSpace G₀] [SeparatelyContinuousMul G₀]
{f : α → G₀} [inst_3 : TopologicalSpace α], Continuous f → ∀ (y : G₀), Continuous fun x => f x / y- Defined in
- Mathlib.Topology.Algebra.GroupWithZero
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Continuousstatement and proof · cited by 2,592
- div_eq_mul_invproof · cited by 715
- SeparatelyContinuousMulstatement and proof · cited by 133
- DivInvMonoidstatement and proof · cited by 103
- Continuous.mul_constproof · cited by 15
Cited by21
Results whose statement or proof uses this declaration.
- Complex.continuous_cosproof · cited by 7
- integral_cpowproof · cited by 5
- Complex.continuous_sinproof · cited by 5
- Real.sin_gt_sub_cubeproof · cited by 2
- summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexpproof · cited by 2
- Function.Periodic.continuous_qParamproof · cited by 2
- Complex.continuous_coshproof · cited by 2
- Complex.continuous_sinhproof · cited by 2
- multipliableUniformlyOn_euler_sin_prod_on_compactproof · cited by 1
- gronwallBound_continuous_εproof · cited by 1
- ODE.FunSpace.dist_iterate_next_apply_leproof · cited by 1
- Complex.approx_Gamma_integral_tendsto_Gamma_integralproof · cited by 1