existsUnique_mem_box

Mathlib.Order.Interval.Finset.Box

URI: https://scilib.ai/kg/mathlib#Int.existsUnique_mem_box

English

For any x ∈ ℤ×ℤ there exists a unique n ∈ ℕ such that x ∈ box(n).

Русский

Для любого x ∈ ℤ×ℤ существует единственный натуральный n такой, что x ∈ box(n).

LaTeX

$$$\exists! n\in\mathbb{N}\;\, x \in \mathrm{box}(n)$$$

Lean4

theorem existsUnique_mem_box (x : ℤ × ℤ) : ∃! n : ℕ, x ∈ box n := by use max x.1.natAbs x.2.natAbs;
  simp only [mem_box, and_self_iff, forall_eq']

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

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

Разделы

Аффилиация

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