existsUnique_congr' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem existsUnique_congr' (h : ∀ b, p (e.symm b) ↔ q b) : (∃! a, p a) ↔ ∃! b, q b :=
  e.existsUnique_congr_left.trans <| by simp [h]

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