existsUnique_congr — Mathlib

English

If p and q are equivalent pointwise, then the existence-uniqueness of x with p x is equivalent to that with q x.

Русский

Если предикаты p и q эквивалентны по всем значениям, то существование-уникальность x для p x эквивалентно существованию-уникальности для q x.

LaTeX

$$$$ (\\\\forall a, p(a) \\\\leftrightarrow q(a)) \Rightarrow (\\\\exists! a, p(a)) \\\\leftrightarrow (\\\\exists! a, q(a)). $$$$

Lean4

theorem existsUnique_congr {p q : α → Prop} (h : ∀ a, p a ↔ q a) : (∃! a, p a) ↔ ∃! a, q a :=
  exists_congr fun _ ↦ and_congr (h _) <| forall_congr' fun _ ↦ imp_congr_left (h _)

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