range_two_mul_add_one

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#range_two_mul_add_one

English

The set {a ∈ α | Odd(a)} is exactly the range of the map x ↦ 2·x + 1.

Русский

Множество {a ∈ α | Odd(a)} совпадает с образами отображения x ↦ 2x + 1.

LaTeX

$$$\\mathrm{range}(\\lambda x:\\alpha,\, 2 \\cdot x + 1) = \\{ a \\mid \\mathrm{Odd}(a) \\}$$$

Lean4

@[simp]
theorem range_two_mul_add_one (α : Type*) [Semiring α] : Set.range (fun x : α ↦ 2 * x + 1) = {a | Odd a} := by ext x;
  simp [Odd, eq_comm]

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

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

Разделы

Аффилиация

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