Commit 2026-02-23 18:16 8aaf32f7

View on Github →

chore(Data/Set/Inclusion): small golf (#34690) Also added inclusion_eq_subtype_map for inclusion h = Subtype.map id h which is true by definition.

Estimated changes

Modified Mathlib/Data/Set/Inclusion.lean

added theorem Set.inclusion_eq_subtype_map

modified theorem Set.inclusion_injective

modified theorem Set.inclusion_right

modified theorem Set.inclusion_self