nhds_zero_of_units — Mathlib

English

If γ is a unit (invertible) in Γ₀, then Iio(γ) is a neighborhood of 0.

Русский

Если γ является единицей (обратимым) в Γ₀, то Iio(γ) — окрестность нуля.

LaTeX

$$$Iio(↑γ) \\in \\mathcal{N}(0) \\quad (γ ∈ Γ₀^×)$$$

Lean4

/-- If `γ` is an invertible element of a linearly ordered group with zero element adjoined, then
`Iio (γ : Γ₀)` is a neighbourhood of `0`. -/
theorem nhds_zero_of_units (γ : Γ₀ˣ) : Iio ↑γ ∈ 𝓝 (0 : Γ₀) :=
  Iio_mem_nhds_zero γ.ne_zero

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