Theorems · Definition · logic and foundations
Function.Embedding.trans
{α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → (α ↪ β) → (β ↪ γ) → α ↪ γComposition of f : α ↪ β and g : β ↪ γ.
- Defined in
- Mathlib.Logic.Embedding.Basic
- Cited by
- 83 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Function.Embeddingstatement and proof · cited by 988
Cited by106
Results whose statement or proof uses this declaration.
- RelEmbedding.transproof · cited by 27
- Function.Embedding.trans_applystatement and proof · cited by 25
- Finset.map_mapstatement and proof · cited by 22
- Int.divisorsAntidiagproof · cited by 17
- Int.divisorsproof · cited by 14
- Nat.finMulAntidiagproof · cited by 13
- Fin.natAdd_castLEEmbproof · cited by 11
- Nat.mem_finMulAntidiagproof · cited by 7
- Int.card_Iccproof · cited by 6
- Int.card_Icoproof · cited by 6
- Function.Embedding.congrproof · cited by 5
- Equiv.asEmbeddingproof · cited by 5