lifts — Mathlib

English

The set lifts x consists of all representations p in FreeAddMonoid (R × Π i, s_i) that map to x under AddCon.toQuotient.

Русский

Множество lifts x состоит из всех представлений p в FreeAddMonoid (R × Π i, s_i), которые отображаются в x через AddCon.toQuotient.

LaTeX

$$$$ \text{lifts}(x) = \{ p \mid \; AddCon.toQuotient(p) = x \} $$$$

Lean4

/-- The set of lifts of an element `x` of `⨂[R] i, s i` in `FreeAddMonoid (R × Π i, s i)`. -/
def lifts (x : ⨂[R] i, s i) : Set (FreeAddMonoid (R × Π i, s i)) :=
  {p | AddCon.toQuotient (c := addConGen (PiTensorProduct.Eqv R s)) p = x}

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