tag_index_eq_self_of_mem_smul_span

English

If x ∈ (n)⁻¹ • L, then tag n (index n x) = x.

Русский

Если x ∈ (n)⁻¹ • L, то tag n (index n x) = x.

LaTeX

$$$$ \mathrm{tag}\, n\, (\mathrm{index}\, n\, x) = x \quad\text{for } x \in (n:\\mathbb{R})^{-1} \cdot L $$$$

Lean4

theorem tag_index_eq_self_of_mem_smul_span {x : ι → ℝ} (hx : x ∈ (n : ℝ)⁻¹ • L) : tag n (index n x) = x :=
  by
  rw [mem_smul_span_iff] at hx
  ext i
  obtain ⟨a, ha⟩ : ∃ a : ℤ, a = n * x i := hx i
  rwa [tag_apply, index_apply, Int.cast_sub, Int.cast_one, sub_add_cancel, ← ha, Int.ceil_intCast,
    div_eq_iff (NeZero.ne _), mul_comm]

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