coe_image_Ico_eq — Mathlib

English

The image of the half-open interval Ico a (a+p) under the quotient map is the entire AddCircle p.

Русский

Образ полускобного интервала Ico a (a+p) под квотированием равен всему AddCircle p.

LaTeX

$$$$ \mathrm{image}\;\mathrm{QuotientAddGroup.mk} \ Ico a (a+p) = \text{univ} $$$$

Lean4

/-- The image of the closed-open interval `[a, a + p)` under the quotient map `𝕜 → AddCircle p` is
the entire space. -/
@[simp]
theorem coe_image_Ico_eq : ((↑) : 𝕜 → AddCircle p) '' Ico a (a + p) = univ :=
  by
  rw [image_eq_range]
  exact (equivIco p a).symm.range_eq_univ

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