tag_mem

Mathlib.Analysis.BoxIntegral.UnitPartition

URI: https://scilib.ai/kg/mathlib#BoxIntegral.unitPartition.tag_mem

← MathLib Explorer

English

The map ν ↦ box(n,ν) is injective.

Русский

Отображение ν ↦ box(n,ν) инъективно.

LaTeX

$$Injective mapping: (ν ↦ box(n,ν)) is injective.$$

Lean4

theorem tag_mem (ν : ι → ℤ) : tag n ν ∈ box n ν :=
  by
  refine mem_box_iff.mpr fun _ ↦ ?_
  rw [tag, add_div]
  have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
  exact ⟨lt_add_of_pos_right _ (by positivity), le_rfl⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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