Theorems · Theorem · logic and foundations
Function.Embedding.mk.congr_simp
∀ {α : Sort u_1} {β : Sort u_2} (toFun toFun_1 : α → β) (e_toFun : toFun = toFun_1) (inj' : Function.Injective toFun),
{ toFun := toFun, inj' := inj' } = { toFun := toFun_1, inj' := ⋯ }- Defined in
- Mathlib.Logic.Embedding.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.Embeddingstatement · cited by 988
Cited by14
Results whose statement or proof uses this declaration.
- Finset.card_Icc_finsetproof · cited by 3
- SimpleGraph.CliqueFree.replaceVertexproof · cited by 3
- Polynomial.coeff_one_reverseproof · cited by 2
- ContextFreeGrammar.reverse_reverseproof · cited by 2
- Finset.mem_finsuppAntidiagproof · cited by 2
- Finset.map_commproof · cited by 1
- Function.Embedding.equiv_symm_toEmbedding_trans_toEmbeddingproof · cited by 1
- Finset.Icc_eq_image_powersetproof · cited by 0
- Finset.finsuppAntidiag_zeroproof · cited by 0
- Fin.Embedding.init_snocproof · cited by 0
- Function.Embedding.equiv_toEmbedding_trans_symm_toEmbeddingproof · cited by 0
- Finset.filter_piFinset_eq_map_consEquivproof · cited by 0