Mathlib Map

Theorems · Theorem · order theory

Set.EqOn.image_eq_self

∀ {α : Type u_1} {s : Set α} {f : α → α}, Set.EqOn f id s → f '' s = s

Variant of EqOn.image_eq, for one function being the identity.

Defined in
Mathlib.Data.Set.Function
Cited by
3 results in Mathlib
Foundations
Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.exists_eq_graphOn_image_fst · cited by 1Set.exists_eq_graphOn_ima…PrimeSpectrum.zeroLocus_minimalPrimes · cited by 1PrimeSpectrum.zeroLocus_m…OpenPartialHomeomorph.extend_left_inv' · cited by 0OpenPartialHomeomorph.ext…Set · cited by 53352SetSet.image · cited by 5609Set.imageSet.EqOn · cited by 603Set.EqOnEqOn.image_eq_selfCITED 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.imagestatement · cited by 5,609
  • Set.EqOnstatement and proof · cited by 603

Cited by3

Results whose statement or proof uses this declaration.