Theorem Set.preimage_fst_singleton_eq_range

Modification history

2025-02-09 06:38
Mathlib/Data/Set/Basic.lean
chore(Data/Set/Basic): split `insert` / `singleton` / `pair` to new file (#21567) …
Modified Set.preimage_fst_singleton_eq_rangeView on Github →
2024-11-03 19:16
Mathlib/Data/Set/Basic.lean
feat: `μ (Prod.fst ⁻¹' {x}) = ∑' y, μ {(x, y)}` (#18390) …
Added Set.preimage_fst_singleton_eq_rangeView on Github →