nonempty_lifts — Mathlib

English

The zero element is lifted by the empty list: 0 ∈ lifts(0).

Русский

Нулевой элемент поднимается пустым списком: 0 ∈ lifts(0).

LaTeX

$$$$ 0 \in \text{lifts}(0) $$$$

Lean4

/-- Every element of `⨂[R] i, s i` has a lift in `FreeAddMonoid (R × Π i, s i)`.
-/
theorem nonempty_lifts (x : ⨂[R] i, s i) : Set.Nonempty (lifts x) :=
  by
  existsi @Quotient.out _ (addConGen (PiTensorProduct.Eqv R s)).toSetoid x
  simp only [lifts, Set.mem_setOf_eq]
  rw [← AddCon.quot_mk_eq_coe]
  erw [Quot.out_eq]

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