existsUnique_congr_right — Mathlib

English

Let e: α ≃ β. Then (∃! a, q(e(a))) ↔ ∃! b, q(b).

Русский

Пусть e: α ≃ β. Тогда (существует единственный a такой, что q(e(a))) эквивалентно существованию единственного b such that q(b).

LaTeX

$$$ \forall e:(\alpha \simeq \beta),\ (\exists! a:\alpha,\ q(e(a))) \leftrightarrow (\exists! b:\beta,\ q(b)) $$$

Lean4

protected theorem existsUnique_congr_right : (∃! a, q (e a)) ↔ ∃! b, q b :=
  e.exists_congr <| by simpa using fun _ _ ↦ e.forall_congr (by simp)

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