exists_subtype_congr — Mathlib

English

If e is an equivalence between subtypes {a | p(a)} and {b | q(b)}, then (∃! a, p(a)) ↔ (∃! b, q(b)).

Русский

Если e — эквивалентность между подтипами {a | p(a)} и {b | q(b)}, то существует единственный элемент с свойством p эквивалентно существованию единственного элемента с свойством q.

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 exists_subtype_congr (e : { a // p a } ≃ { b // q b }) : (∃ a, p a) ↔ ∃ b, q b := by
  simp [← nonempty_subtype, nonempty_congr e]

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