Mathlib Map

Theorems · Theorem · group theory

Set.inv_preimage

∀ {α : Type u_2} [inst : Inv α] {s : Set α}, Inv.inv ⁻¹' s = s⁻¹
Defined in
Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by
4 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Inv
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MeasureTheory.quasiMeasurePreserving_inv · cited by 7MeasureTheory.quasiMeasur…Finset.preimage_inv · cited by 0Finset.preimage_invFilter.inv_mem_inv · cited by 0Filter.inv_mem_invMeasureTheory.eventuallyConst_inv_set_ae · cited by 0MeasureTheory.eventuallyC…Set · cited by 53352SetSet.preimage · cited by 4946Set.preimageSet.inv · cited by 132Set.invSet.inv_preimageCITED BYCITES

Cites3

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.preimagestatement · cited by 4,946
  • Set.invstatement · cited by 132

Cited by4

Results whose statement or proof uses this declaration.