existsUnique_congr_left — Mathlib

English

Let e: α ≃ β. Then (∃! a, p(a)) ↔ ∃! b, p(e^{-1}(b)).

Русский

Пусть e: α ≃ β. Тогда (существует единственный a, такой что p(a)) эквивалентно существованию единственного b такого, что p(e^{-1}(b)).

LaTeX

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

Lean4

protected theorem existsUnique_congr_left : (∃! a, p a) ↔ ∃! b, p (e.symm b) :=
  e.symm.existsUnique_congr_right.symm

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