Commit 2022-12-24 08:14 19282527

View on Github →

feat: port Data.Set.UnionLift (#1193)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/UnionLift.lean

added theorem Set.liftCover_coe

added theorem Set.liftCover_of_mem

added theorem Set.unionᵢLift_binary

added theorem Set.unionᵢLift_const

added theorem Set.unionᵢLift_inclusion

added theorem Set.unionᵢLift_mk

added theorem Set.unionᵢLift_of_mem

added theorem Set.unionᵢLift_unary