English
If f is bijective, then for any predicate p on β, (∃! y, p(y)) ↔ (∃! x, p(f(x))).
Русский
Пусть f биективна. Тогда для любого свойства p на β: существует единичный элемент y с p(y) тогда и только тогда существует единственный x с p(f(x)).
LaTeX
$$$\operatorname{Bijective}(f) \Rightarrow \forall p:\beta \to \text{Prop}, \big(\exists! y:\beta, p(y)\big) \iff \big(\exists! x:\alpha, p(f(x))\big).$$$
Lean4
theorem existsUnique_iff {f : α → β} (hf : Bijective f) {p : β → Prop} : (∃! y, p y) ↔ ∃! x, p (f x) :=
⟨fun ⟨y, hpy, hy⟩ ↦
let ⟨x, hx⟩ := hf.surjective y
⟨x, by simpa [hx], fun z (hz : p (f z)) ↦ hf.injective <| hx.symm ▸ hy _ hz⟩,
fun ⟨x, hpx, hx⟩ ↦
⟨f x, hpx, fun y hy ↦
let ⟨z, hz⟩ := hf.surjective y
hz ▸ congr_arg f (hx _ (by simpa [hz]))⟩⟩
