forall_congr' — Mathlib

English

Let e be a bijection α ≃ β. If for all b in β, p(e^{-1}(b)) is equivalent to q(b), then (∀a, p(a)) ↔ (∀b, q(b)).

Русский

Пусть e — биекция α ≃ β. Если для каждого b ∈ β выполняется p(e^{-1}(b)) ⇔ q(b), то (∀a, p(a)) ↔ (∀b, q(b)).

LaTeX

$$$ \forall e:(\alpha \simeq \beta),\ (\forall b:\beta,\ p(e^{-1}(b)) \leftrightarrow q(b)) \rightarrow (\forall a:\alpha,\ p(a)) \leftrightarrow (\forall b:\beta,\ q(b)) $$$

Lean4

protected theorem forall_congr' (h : ∀ b, p (e.symm b) ↔ q b) : (∀ a, p a) ↔ ∀ b, q b :=
  e.forall_congr_left.trans (by simp [h])

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