English
If e: α ≃ β is a bijection, then a property p on subsets of α is true for all subsets of α if and only if it is true for all preimages of subsets of β under e.
Русский
Пусть e: α ≃ β — биекция. Тогда свойство p над подмножествами α истинно для всех подмножеств α тогда и лишь тогда, когда оно истинно для всех предобразов подмножеств β по e.
LaTeX
$$$\\forall e:\\alpha\\cong\\beta\\,\\forall p:\\mathcal{P}(\\alpha)\\to\\mathrm{Prop},\\; (\\forall A\\subseteq\\alpha,\\; p(A)) \\iff (\\forall B\\subseteq\\beta,\\; p(e^{-1}[B]))$$$
Lean4
protected theorem set_forall_iff {α β} (e : α ≃ β) {p : Set α → Prop} : (∀ a, p a) ↔ ∀ a, p (e ⁻¹' a) :=
e.injective.preimage_surjective.forall
