Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-12-15 13:12
d08e3e0d
View on Github →
feat(Set/Lattice): add
Set.seq_eq_image2
, use it to golf some proofs (
#9062
)
Estimated changes
Modified
Mathlib/Data/Set/Lattice.lean
modified
theorem
Set.iUnion_image_right
modified
theorem
Set.seq_def
added
theorem
Set.seq_eq_image2
modified
theorem
Set.seq_singleton
modified
theorem
Set.singleton_seq