Commit 2023-07-25 13:48 3b24f007

View on Github →

feat: basic set lemmas (#6010)

Estimated changes

Modified Mathlib/Analysis/BoundedVariation.lean

deleted theorem Set.subsingleton_Icc_of_ge

Modified Mathlib/Data/Set/Intervals/Basic.lean

added theorem Set.subsingleton_Icc_iff

added theorem Set.subsingleton_Icc_of_ge

Modified Mathlib/Data/Set/Pairwise/Basic.lean

added theorem Set.exists_lt_mem_inter_of_not_pairwiseDisjoint

added theorem Set.exists_ne_mem_inter_of_not_pairwiseDisjoint

added theorem exists_lt_mem_inter_of_not_pairwise_disjoint

added theorem exists_ne_mem_inter_of_not_pairwise_disjoint

Modified Mathlib/Topology/ContinuousFunction/Weierstrass.lean