frequently_odd

Mathlib.Order.Filter.AtTopBot.ModEq

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

English

There are infinitely many even natural numbers.

Русский

Существует бесконечно много чётных натуральных чисел.

LaTeX

$$$\\exists^{\\infty} m \\in \\operatorname{atTop},\\; \\text{Even}(m)$$$

Lean4

theorem frequently_odd : ∃ᶠ m : ℕ in atTop, Odd m := by simpa only [odd_iff] using frequently_mod_eq one_lt_two

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

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

Разделы

Аффилиация

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