Commit 2026-08-16 17:38 a7cadaed

View on Github →

chore(Data/Set): add missing Set.forall_mem_* lemmas (#42549) Add lemmas Set.forall_mem_inter, Set.forall_mem_union, Set.forall_mem_singleton, Set.forall_mem_univ, Set.forall_mem_iUnion, Set.forall_mem_iUnion₂, Set.forall_mem_biUnion, and their exists counterparts.

Estimated changes

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.Nonempty.exists_const

added theorem Set.exists_mem_const

added theorem Set.exists_mem_empty

added theorem Set.exists_mem_inter

added theorem Set.exists_mem_ofPred

added theorem Set.exists_mem_union

added theorem Set.exists_mem_univ

added theorem Set.forall_mem_inter

added theorem Set.forall_mem_ofPred

added theorem Set.forall_mem_union

added theorem Set.forall_mem_univ

Modified Mathlib/Data/Set/Insert.lean

added theorem Set.exists_mem_singleton

added theorem Set.forall_mem_singleton

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.exists_mem_biUnion

added theorem Set.exists_mem_iUnion

added theorem Set.exists_mem_iUnion₂

added theorem Set.forall_mem_biUnion

added theorem Set.forall_mem_iUnion

added theorem Set.forall_mem_iUnion₂