isCompl_even_odd

Mathlib.Algebra.Order.Ring.Nat

URI: https://scilib.ai/kg/mathlib#Nat.isCompl_even_odd

English

The sets {n ∈ ℕ | Even n} and {n ∈ ℕ | Odd n} are complements.

Русский

Множества чётных и нечётных чисел комплементарны.

LaTeX

$$IsCompl {n ∈ \\mathbb{N} : \\text{Even}(n)} {n ∈ \\mathbb{N} : \\text{Odd}(n)}$$

Lean4

theorem isCompl_even_odd : IsCompl {n : ℕ | Even n} {n | Odd n} := by
  simp only [← Set.compl_setOf, isCompl_compl, ← not_even_iff_odd]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru