Mathlib Map

Theorems · Theorem · order theory

Set.image_singleton

∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α}, f '' {a} = {f a}
Defined in
Mathlib.Data.Set.Image
Cited by
174 results in Mathlib
Foundations
Depth 16 from the axioms, rests on 74 definitions · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

nhdsSet_singleton · cited by 19nhdsSet_singletonFinset.map_singleton · cited by 15Finset.map_singletonSet.image_injective · cited by 15Set.image_injectiveSet.neg_singleton · cited by 14Set.neg_singletonAlgebra.adjoin_singleton_eq_range_aeval · cited by 12Algebra.adjoin_singleton_…Topology.IsInducing.specializes_iff · cited by 10IsInducing.specializes_iffSubmonoid.map_powers · cited by 10Submonoid.map_powersSet.image2_singleton · cited by 10Set.image2_singletonSet.inv_singleton · cited by 9Set.inv_singletonchartedSpaceSelf_prod · cited by 9chartedSpaceSelf_prodt1Space_TFAE · cited by 8t1Space_TFAEAddMonoidHom.map_zmultiples · cited by 6AddMonoidHom.map_zmultipl…Set.vadd_set_singleton · cited by 6Set.vadd_set_singletonSet.image_one · cited by 5Set.image_oneSet.smul_set_singleton · cited by 5Set.smul_set_singletonSet · cited by 53352SetSet.image · cited by 5609Set.imageSet.image_singletonCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • Set.imagestatement · cited by 5,609

Cited by174

Results whose statement or proof uses this declaration.