coe_image_Ioc_eq — Mathlib

English

The image of the closed-open interval Ioc a (a+p) under the quotient map is the entire universe of AddCircle p.

Русский

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

LaTeX

$$$$ \mathrm{image}\;\mathrm{QuotientAddGroup.mk} \ Ioc 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_Ioc_eq : ((↑) : 𝕜 → AddCircle p) '' Ioc a (a + p) = univ :=
  by
  rw [image_eq_range]
  exact (equivIoc p a).symm.range_eq_univ

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