Theorems · Theorem · logic and foundations
Subtype.map_injective
∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ (a : α), p a → q (f a)),
Function.Injective f → Function.Injective (Subtype.map f h)- Defined in
- Mathlib.Data.Subtype
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Subtype.coe_injectiveproof · cited by 205
- Subtype.mapstatement · cited by 52
- Subtype.coind_injectiveproof · cited by 4
Cited by7
Results whose statement or proof uses this declaration.
- Set.inclusion_injectiveproof · cited by 28
- Finset.prod_addproof · cited by 7
- Finset.filter_attach'statement · cited by 2
- CategoryTheory.ObjectProperty.Small.of_leproof · cited by 0
- StarSubalgebra.isEmbedding_inclusionproof · cited by 0
- Unitary.map_injectiveproof · cited by 0
- Equiv.Perm.CycleType.count_defproof · cited by 0