existsUnique_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 existsUnique_congr (h : ∀ a, p a ↔ q (e a)) : (∃! a, p a) ↔ ∃! b, q b :=
  e.existsUnique_congr_left.trans <| by simp [h]

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