Theorems · Theorem · group theory
Set.image_inv_eq_inv
∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, (fun x => x⁻¹) '' s = s⁻¹- Cited by
- 44 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses propext, Quot.sound
- Assumes
- InvolutiveInv
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.imagestatement · cited by 5,609
- Set.invstatement · cited by 132
- InvolutiveInvstatement and proof · cited by 102
- Set.image_eq_preimage_of_inverseproof · cited by 27
- inv_involutiveproof · cited by 12
- Function.Involutive.leftInverseproof · cited by 5
- Function.Involutive.rightInverseproof · cited by 4
Cited by44
Results whose statement or proof uses this declaration.
- Set.inv_singletonproof · cited by 9
- Cardinal.mk_Ioo_realproof · cited by 5
- IsCompact.invproof · cited by 4
- Finset.coe_invproof · cited by 3
- inv_atTop₀proof · cited by 3
- Set.finite_invproof · cited by 3
- Convex.closure_subset_image_homothety_interior_of_one_ltproof · cited by 2
- infEDist_inv_invproof · cited by 2
- inv_atBot₀proof · cited by 2
- Set.inv_rangeproof · cited by 2
- Set.image_const_div_Iioproof · cited by 1
- Set.image_const_div_Ioiproof · cited by 1