Commit 2022-11-30 20:20 5213b203

View on Github →

feat: port Order.RelIso.Basic (#772) SHA 19091d8f2e537e76a81d1608e011dd4d03f94642 Finished the port

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/RelIso/Basic.lean

added def RelEmbedding.Simps.apply

added theorem RelEmbedding.coe_fn_injective

added theorem RelEmbedding.coe_trans

added theorem RelEmbedding.eq_preimage

added theorem RelEmbedding.ext

added theorem RelEmbedding.ext_iff

added theorem RelEmbedding.inj

added theorem RelEmbedding.injective

added theorem RelEmbedding.map_rel_iff

added def RelEmbedding.ofIsEmpty

added def RelEmbedding.ofMapRelIff

added theorem RelEmbedding.ofMapRelIff_coe

added def RelEmbedding.ofMonotone

added theorem RelEmbedding.ofMonotone_coe

added def RelEmbedding.preimage

added def RelEmbedding.prodLexMap

added def RelEmbedding.prodLexMkLeft

added def RelEmbedding.prodLexMkRight

added def RelEmbedding.sumLexInl

added def RelEmbedding.sumLexInr

added def RelEmbedding.sumLexMap

added def RelEmbedding.sumLiftRelInl

added def RelEmbedding.sumLiftRelInr

added def RelEmbedding.sumLiftRelMap

added def RelEmbedding.toRelHom

added theorem RelEmbedding.trans_apply

added structure RelEmbedding

added theorem RelHom.coe_fn_injective

added theorem RelHom.coe_fn_toFun

added theorem RelHom.ext

added theorem RelHom.ext_iff

added theorem RelHom.injective_of_increasing

added def RelHom.preimage

added structure RelHom

added def RelIso.Simps.apply

added def RelIso.Simps.symmApply

added theorem RelIso.apply_symm_apply

added theorem RelIso.coe_fn_injective

added theorem RelIso.coe_fn_mk

added theorem RelIso.coe_fn_symm_mk

added theorem RelIso.coe_fn_toEquiv

added theorem RelIso.default_def

added theorem RelIso.eq_iff_eq

added theorem RelIso.ext

added theorem RelIso.ext_iff

added theorem RelIso.map_rel_iff

added def RelIso.prodLexCongr

added def RelIso.relIsoOfIsEmpty

added def RelIso.relIsoOfUniqueOfIrrefl

added def RelIso.relIsoOfUniqueOfRefl

added theorem RelIso.rel_symm_apply

added def RelIso.sumLexCongr

added theorem RelIso.symm_apply_apply

added theorem RelIso.symm_apply_rel

added theorem RelIso.toEquiv_injective

added def RelIso.toRelEmbedding

added structure RelIso

added def Subtype.relEmbedding

added theorem Surjective.wellFounded_iff

added theorem injective_of_increasing

added theorem preimage_equivalence

added theorem wellFounded_lift₂_iff