Theorem Finset.map_truncatedSup

Modification history

2025-03-17 06:31
Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
chore: Migrate to `DecidableLT` and `DecidableLE` (#22238) …
Modified Finset.map_truncatedSupView on Github →
2024-12-11 04:11
Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
chore: used named arguments instead of @DecidableRel (#19850)
Modified Finset.map_truncatedSupView on Github →
2024-08-01 16:02
Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
chore: backports for leanprover/lean4#4814 (part 11) (#15394) …
Modified Finset.map_truncatedSupView on Github →
2024-01-09 07:03
Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
feat: The Ahlswede-Zhang identity (#8171) …
Added Finset.map_truncatedSupView on Github →