setOf_mem_integer_eq_closedBall — Mathlib

English

Let L be as above. The set of elements with integer valuation equals the closed unit ball, i.e., { x ∈ L : v(x) ∈ Z } = { x ∈ L : ‖x‖ ≤ 1 }.

Русский

Пусть L имеет заданную векторную оценку; множество элементов с целочисленным значением равно замкнутому шару радиуса 1: { x ∈ L : v(x) ∈ Z } = { x ∈ L : ‖x‖ ≤ 1 }.

LaTeX

$$$\{x \in L : v(x) \in \mathbb{Z}\} = \{x \in L : \|x\| \le 1\}$$$

Lean4

theorem setOf_mem_integer_eq_closedBall : {x : L | x ∈ Valued.v.integer} = Metric.closedBall 0 1 :=
  by
  ext x
  simp [mem_integer_iff]

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