exists — Mathlib

English

For any property P on ZMod n, there exists a residue with that property iff there exists an integer whose cast has that property.

Русский

Для любого свойства P на ZMod n существует класс остатка с данным свойством тогда и только тогда, когда существует целое число, чье приведение обладает данным свойством.

LaTeX

$$$\\\\forall {n} \\\\forall {P : ZMod n \\\\to \\\\mathrm{Prop}}, \\\\bigl( \\\\exists x : ZMod n, P x \bigr) \\\\iff \\\\bigl( \\\\exists z : \\\\mathbb{Z}, P z \bigr)$$$

Lean4

theorem «exists» {P : ZMod n → Prop} : (∃ x, P x) ↔ ∃ x : ℤ, P x :=
  intCast_surjective.exists

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