Theorems · Theorem · group theory
Set.zero_smul_set
∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] {s : Set β},
s.Nonempty → 0 • s = 0A nonempty set is scaled by zero to the singleton set containing 0.
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext, Quot.sound
- Assumes
- ZeroZeroSMulWithZero
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.
- Setstatement and proof · cited by 53,352
- Set.Nonemptystatement and proof · cited by 2,627
- zero_smulproof · cited by 716
- Set.smulSetstatement · cited by 608
- Set.image_congrproof · cited by 533
- SMulWithZerostatement and proof · cited by 113
- Set.zerostatement · cited by 87
- Set.Nonempty.image_constproof · cited by 26
Cited by20
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.addHaar_smulproof · cited by 13
- smul_closedBallproof · cited by 6
- egauge_zero_rightproof · cited by 4
- Real.sInf_smul_of_nonnegproof · cited by 3
- Finset.zero_smul_finsetproof · cited by 2
- fderiv_comp_smulproof · cited by 2
- balancedCore_nonempty_iffproof · cited by 2
- smul_sphereproof · cited by 1
- ediam_smul₀proof · cited by 1
- ConvexBody.smul_le_of_leproof · cited by 1
- IsOpen.balancedHullproof · cited by 1
- Real.sInf_smul_of_nonposproof · cited by 1