English
In the integers, the set of even numbers and the set of odd numbers are complements: every integer is either even or odd and they are disjoint.
Русский
В целых числах множества чётных и нечётных чисел взаимно дополняют друг друга: каждый целый либо чётный, либо нечётный, и они не перекрываются.
LaTeX
$$IsCompl\{n\in \mathbb{Z} \mid \text{Even}(n)\} \{n\in \mathbb{Z} \mid \text{Odd}(n)\}$$
Lean4
theorem isCompl_even_odd : IsCompl {n : ℤ | Even n} {n | Odd n} := by
simp [← not_even_iff_odd, ← Set.compl_setOf, isCompl_compl]