Theorems · Theorem
Function.extend_injective
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
Function.Injective f → ∀ (e' : β → γ), Function.Injective fun g => Function.extend f g e'- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Function.extendstatement and proof · cited by 111
- Function.Injective.extend_applyproof · cited by 57
Cited by2
Results whose statement or proof uses this declaration.
- strongRankCondition_iff_succproof · cited by 4
- strongRankCondition_iff_forall_zero_lt_finrankproof · cited by 0