Commit 2024-04-04 09:42 b918ee96

feat(Logic/Equiv/Set): image of equiv applied to setOf (#11628) Add a lemma about the image of an equiv applied to setOf:

lemma setOf_apply_symm_eq_image_setOf {α β} (e : α ≃ β) (p : α → Prop) :
    {b | p (e.symm b)} = e '' {a | p a} := by

From AperiodicMonotilesLean.