Commit 2022-12-14 09:34 04b02cba

View on Github →

feat port: Order.RelIso.Set (#1005) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/RelIso/Set.lean

added def RelEmbedding.codRestrict

added theorem RelEmbedding.codRestrict_apply

added theorem RelHomClass.map_inf

added theorem RelHomClass.map_sup

added theorem RelIso.range_eq

added theorem Subrel.relEmbedding_apply

added def Subrel

added theorem subrel_val