Theorems · Theorem · group theory
Set.mem_vadd_set_iff_neg_vadd_mem
∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {A : Set β} {a : α} {x : β},
x ∈ a +ᵥ A ↔ -a +ᵥ x ∈ A- Cited by
- 24 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, 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.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- Set.imageproof · cited by 5,609
- AddGroupstatement and proof · cited by 4,410
- HVAdd.hVAddstatement and proof · cited by 1,820
- AddActionstatement and proof · cited by 820
- Set.vaddSetstatement · cited by 403
- Set.mem_image_equivproof · cited by 22
- AddAction.toPermproof · cited by 21
Cited by24
Results whose statement or proof uses this declaration.
- AddAction.mem_stabilizer_setproof · cited by 5
- MeasureTheory.IsAddFundamentalDomain.mk'proof · cited by 3
- isClosed_setOfPred_isCompactOperatorproof · cited by 3
- AddSubgroup.leftCoset_cover_filter_FiniteIndex_auxproof · cited by 3
- vadd_coe_setproof · cited by 3
- IsIntegralCurveOn.comp_addproof · cited by 2
- cauchy_davenport_minOrder_addproof · cited by 2
- op_vadd_coe_setproof · cited by 2
- AddAction.fixedBy_mem_fixedBy_of_addCommuteproof · cited by 2
- QuotientAddGroup.soundproof · cited by 2
- Finset.card_vadd_inter_vaddproof · cited by 2
- QuotientAddGroup.orbit_mk_eq_vaddproof · cited by 1