English
Let e be a bijection between α and β. If for every a in α, p(a) is equivalent to q(e(a)), then the universal statements ∀a∈α, p(a) and ∀b∈β, q(b) are equivalent.
Русский
Пусть e — биекция между множествами α и β. Если для каждого элемента a ∈ α выполняется p(a) ⇔ q(e(a)), то тождество ∀a ∈ α, p(a) эквивалентно ∀b ∈ β, q(b).
LaTeX
$$$ \forall e:(\alpha \simeq \beta),\ (\forall a:\alpha,\ p(a) \leftrightarrow q(e(a))) \rightarrow (\forall a:\alpha,\ p(a)) \leftrightarrow (\forall b:\beta,\ q(b)) $$$
Lean4
protected theorem forall_congr (h : ∀ a, p a ↔ q (e a)) : (∀ a, p a) ↔ ∀ b, q b :=
e.forall_congr_left.trans (by simp [h])
