Commit 2023-12-22 20:59 763e4db0

View on Github →

chore(*): use Set.image2_subset_iff (#9206) Use Set.image2_subset_iff, Set.mul_subset_iff, and Set.add_subset_iff instead of rintros. Also protect some *.image2 lemmas.

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

Modified Mathlib/GroupTheory/Submonoid/Pointwise.lean

modified theorem Submonoid.mul_subset

Modified Mathlib/Order/Bounds/Basic.lean

deleted theorem BddAbove.image2

deleted theorem BddBelow.image2

deleted theorem IsGreatest.image2

deleted theorem IsLeast.image2

Modified Mathlib/RingTheory/Adjoin/FG.lean