equivIocMod_coe — Mathlib

English

The canonical map sending a representative in the quotient to its corresponding IocMod image is compatible with the standard coe to α.

Русский

Каноническое отображение, отправляющее представитель фактор-группы в соответствующее изображение IocMod, согласуется с естественным включением в α.

LaTeX

$$$$ \\text{QuotientAddGroup}.equivIocMod\\; hp\\; a\\; 0 = \\langle \\operatorname{toIocMod}(hp, a, 0), \\operatorname{toIocMod\_mem\_Ioc}(hp, a, 0) \\rangle $$$$

Lean4

@[simp]
theorem equivIocMod_coe (a b : α) : QuotientAddGroup.equivIocMod hp a ↑b = ⟨toIocMod hp a b, toIocMod_mem_Ioc hp a _⟩ :=
  rfl

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