Mathlib Map

Theorems · Theorem · group theory

Set.image_vadd

∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {t : Set β} {a : α}, (fun x => a +ᵥ x) '' t = a +ᵥ t
Defined in
Mathlib.Algebra.Group.Pointwise.Set.Scalar
Cited by
6 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
VAdd
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AddAction.IsPretransitive.discreteTopology_iff · cited by 2IsPretransitive.discreteT…MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zero · cited by 2Measure.pairwise_aedisjoi…MeasureTheory.IsAddFundamentalDomain.aestronglyMeasurable_on_iff · cited by 1IsAddFundamentalDomain.ae…AddAction.IsTrivialBlock.vadd · cited by 1IsTrivialBlock.vaddAddAction.IsPretransitive.t1Space_iff · cited by 1IsPretransitive.t1Space_i…AddAction.isMultiplyPreprimitive_succ_iff_ofStabilizer · cited by 0AddAction.isMultiplyPrepr…Set · cited by 53352SetSet.image · cited by 5609Set.imageHVAdd.hVAdd · cited by 1820HVAdd.hVAddVAdd · cited by 616VAddSet.vaddSet · cited by 403Set.vaddSetSet.image_vaddCITED BYCITES

Cites5

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.imagestatement · cited by 5,609
  • HVAdd.hVAddstatement · cited by 1,820
  • VAddstatement and proof · cited by 616
  • Set.vaddSetstatement · cited by 403

Cited by6

Results whose statement or proof uses this declaration.