Theorem Set.pi_iUnion_eq_iInter_pi

Modification history

2026-08-24 10:14
Mathlib/Data/Set/Lattice.lean
refactor(Data/Set): split long file Lattice.lean (#43030) …
Modified Set.pi_iUnion_eq_iInter_piView on Github →
2025-12-03 01:23
Mathlib/Data/Set/Lattice.lean
feat(Probability): version of `infinitePi_pi` for countable sets (#32287)
Added Set.pi_iUnion_eq_iInter_piView on Github →