eq_coe_Ico — Mathlib

English

The AddCircle p corresponds to the interval Ico a (a+p) via the quotient IcoMod map, i.e., every AddCircle element is represented by some x in Ico a (a+p).

Русский

AddCircle p эквивалентно интервалу Ico a (a+p) через отображение quotient IcoMod, то есть каждый элемент AddCircle имеет представитель в Ico a (a+p).

LaTeX

$$$$ \exists x, x \in Ico\ a\ (a+p) \text{ and } (x : AddCircle\ p) = a(x) $$$$

Lean4

theorem eq_coe_Ico (a : AddCircle p) : ∃ b, b ∈ Ico 0 p ∧ ↑b = a :=
  by
  let b := QuotientAddGroup.equivIcoMod hp.out 0 a
  exact ⟨b.1, by simpa only [zero_add] using b.2, (QuotientAddGroup.equivIcoMod hp.out 0).symm_apply_apply a⟩

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