setOf_apply_symm_eq_image_setOf — Mathlib

English

For a bijection e and any predicate p on α, the set {b | p(e^{-1} b)} equals the image under e of {a | p(a)}.

Русский

Для биекции e и предиката p на α верно: {b | p(e^{-1} b)} равно образу e от {a | p(a)}.

LaTeX

$$$ \{b \mid p(e^{-1} b)\} = e''\{a \mid p(a)\} $$$

Lean4

theorem setOf_apply_symm_eq_image_setOf {α β} (e : α ≃ β) (p : α → Prop) : {b | p (e.symm b)} = e '' {a | p a} := by
  rw [Equiv.image_eq_preimage, preimage_setOf_eq]

Похожие утверждения