quotientInfToPiQuotient_mk' — Mathlib

English

A variant of Mk mapping for the iInf index set: (iInf I) index yields projections to each I_i.

Русский

Вариант отображения Mk для iInf, при котором индексация по iInf даёт проекции в каждый I_i.

LaTeX

$$$\text{quotientInfToPiQuotient } I (\operatorname{Quotient.mk} (iInf i \mapsto I_i) x) i = \operatorname{Quotient.mk}(I_i) x$$$

Lean4

theorem quotientInfToPiQuotient_mk' (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] (x : R) (i : ι) :
    quotientInfToPiQuotient I (Quotient.mk _ x) i = Quotient.mk (I i) x :=
  rfl

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