exists_congr — Mathlib

English

Let e: α ≃ β. If ∀ a, p(a) ↔ q(e(a)), then (∃ a, p(a)) ↔ (∃ b, q(b)).

Русский

Пусть 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 (\exists a:\alpha,\ p(a)) \leftrightarrow (\exists b:\beta,\ q(b)) $$$

Lean4

protected theorem exists_congr (h : ∀ a, p a ↔ q (e a)) : (∃ a, p a) ↔ ∃ b, q b :=
  e.exists_congr_left.trans <| by simp [h]

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