Theorems · Theorem
Function.Injective.extend_apply
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
Function.Injective f → ∀ (g : α → γ) (e' : β → γ) (a : α), Function.extend f g e' (f a) = g a- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 57 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Function.extendstatement · cited by 111
- Function.FactorsThrough.extend_applyproof · cited by 6
- Function.Injective.factorsThroughproof · cited by 4
Cited by57
Results whose statement or proof uses this declaration.
- Function.extend_compproof · cited by 10
- Function.extend_val_applyproof · cited by 5
- ProbabilityTheory.Kernel.iIndepSets.precompproof · cited by 4
- MeasurableEmbedding.stronglyMeasurable_extendproof · cited by 4
- Cardinal.toENatAux_natproof · cited by 4
- Finset.prod_eq_prod_extendproof · cited by 3
- ContMDiff.inlproof · cited by 3
- ContMDiff.inrproof · cited by 3
- four_functions_theoremproof · cited by 3
- MeasureTheory.SimpleFunc.extend_applyproof · cited by 3
- Polynomial.card_support_eqproof · cited by 3
- cfcₙHom_eq_cfcₙ_extendproof · cited by 3