Theorems · Theorem · order theory
Set.image_id
∀ {α : Type u_1} (s : Set α), id '' s = s- Defined in
- Mathlib.Data.Set.Image
- Cited by
- 60 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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.image_congrproof · cited by 533
- Set.image_id'proof · cited by 86
Cited by60
Results whose statement or proof uses this declaration.
- IsOpenMap.idproof · cited by 12
- IsClosedMap.idproof · cited by 8
- Submodule.fg_of_fg_map_of_fg_inf_kerproof · cited by 7
- MeasurableEmbedding.idproof · cited by 7
- Submodule.mem_span_setproof · cited by 6
- Subgroup.map_idproof · cited by 4
- IsPreconnected.Icc_subsetproof · cited by 4
- Submodule.mem_span_iff_exists_finset_subsetproof · cited by 3
- AffineSubspace.map_idproof · cited by 3
- LinearIndepOn.id_insertproof · cited by 3
- AddSubgroup.map_idproof · cited by 3
- Set.compl_compl_imageproof · cited by 2