ceil_eq_self_of_mem — Mathlib

English

The ceil map is defined as the sum over i of the ceiling of the i-th coordinate times the i-th basis vector in the integer-span lattice.

Русский

ceil по базису b определяется как сумма по i ⌈b.repr(m)_i⌉ · b.restrictScalarsℤ i.

LaTeX

$$$ \operatorname{ceil}_b(m) = \sum_i \lceil b.repr(m)_i \rceil \; b.restrictScalars \mathbb{Z}_i $$$

Lean4

@[simp]
theorem ceil_eq_self_of_mem (m : E) (h : m ∈ span ℤ (Set.range b)) : (ceil b m : E) = m :=
  by
  apply b.ext_elem
  simp_rw [repr_ceil_apply b]
  intro i
  obtain ⟨z, hz⟩ := (b.mem_span_iff_repr_mem ℤ _).mp h i
  rw [← hz]
  exact congr_arg (Int.cast : ℤ → K) (Int.ceil_intCast z)

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