English
If e is an equivalence between subtype {a | p(a)} and {b | q(b)}, then (∃! a, p(a)) ↔ ∃! b, q(b).
Русский
Если e — эквивалент между подтипами {a | p(a)} и {b | q(b)}, то существует единственный элемент в каждом подтипе эквивалентно друг другу.
LaTeX
$$$ \forall e:(\{a:\alpha // p(a)\} \simeq \{b:\beta // q(b)\}),\ (\exists! a:\alpha,\ p(a)) \leftrightarrow (\exists! b:\beta,\ q(b)) $$$
Lean4
protected theorem existsUnique_subtype_congr (e : { a // p a } ≃ { b // q b }) : (∃! a, p a) ↔ ∃! b, q b := by
simp [← unique_subtype_iff_existsUnique, unique_iff_subsingleton_and_nonempty, nonempty_congr e, subsingleton_congr e]
-- We next build some higher arity versions of `Equiv.forall_congr`.
-- Although they appear to just be repeated applications of `Equiv.forall_congr`,
-- unification of metavariables works better with these versions.
-- In particular, they are necessary in `equiv_rw`.
-- (Stopping at ternary functions seems reasonable: at least in 1-categorical mathematics,
-- it's rare to have axioms involving more than 3 elements at once.)
