quotMk_of — Mathlib

English

The quotient construction that represents direct sums corresponds to the canonical embedding: quot of the component (i, x) equals the embedding of x.

Русский

Квотирование, представляющее прямую сумму, соответствует каноническому вложению: Quot.mk из (i, x) совпадает с образованием of(i, x).

LaTeX

$$$\\operatorname{Quot.mk}_{\\rm setoid}(\\, \\text{DirectLimit} \\text{setoid } f\\,)(\\langle i, x \\rangle) = \\text{of}(R, \\iota, G, f, i, x)$$$

Lean4

theorem quotMk_of (i x) : Quot.mk _ (.of G i x) = of R ι G f i x :=
  rfl

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