Theorem Finset.mem_union_of_disjoint

Modification history

2025-09-05 03:04
Mathlib/Data/Finset/Basic.lean
feat(Data/{Set, Finset}): a few easy lemmas about `Set.univ (Finset a)` and `Set.univ (Set a)` (#29238) …
Modified Finset.mem_union_of_disjointView on Github →
2025-07-10 04:21
Mathlib/Data/Finset/Basic.lean
feat: {Set,Finset}.mem_union_of_disjoint (#26946)
Added Finset.mem_union_of_disjointView on Github →