Commit 2024-12-10 14:59 b7e27175

View on Github →

chore: rename forall_image2_iff to forall_mem_image2 (#19401) This matches the existing image lemmas. Also add the missing exists lemma. From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean

Modified Mathlib/Combinatorics/SetFamily/Shatter.lean

Modified Mathlib/Data/Finset/Image.lean

added theorem Finset.exists_mem_image

deleted theorem Finset.forall_image

added theorem Finset.forall_mem_image

Modified Mathlib/Data/Finset/NAry.lean

added theorem Finset.exists_mem_image₂

deleted theorem Finset.forall_image₂_iff

added theorem Finset.forall_mem_image₂

Modified Mathlib/Data/Finset/Sups.lean

Modified Mathlib/Data/Set/NAry.lean

added theorem Set.exists_mem_image2

deleted theorem Set.forall_image2_iff

added theorem Set.forall_mem_image2

Modified Mathlib/Data/Set/Sups.lean

Modified Mathlib/Dynamics/OmegaLimit.lean

Modified Mathlib/NumberTheory/MaricaSchoenheim.lean

Modified Mathlib/Order/Bounds/Image.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/EMetricSpace/Lipschitz.lean