coe_span_singleton_eq_closedBall — Mathlib

English

The ideal generated by a singleton in the valuation ring equals the closed ball of radius ‖x‖ around 0.

Русский

Идеал, порожденный единичным элементом x в 𝒪[K], равен замкнутому шару радиуса ‖x‖ вокруг 0.

LaTeX

$$$$ (\mathrm{Ideal.span}\{x\} : \mathrm{Set} 𝒪[K]) = \mathrm{Metric.closedBall}(0, \|x\|), $$$$

Lean4

theorem coe_span_singleton_eq_closedBall (x : 𝒪[K]) : (Ideal.span { x } : Set 𝒪[K]) = Metric.closedBall 0 ‖x‖ := by
  simp [Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe, Set.ext_iff, ← NNReal.coe_le_coe]

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