mk — Mathlib · SciLib

English

There is a constructor that packages a function x: ∏ i R_i together with a proof that almost every x_i belongs to A_i, into an element of the restricted product.

Русский

Существуют конструкция mk, которая объединяет функцию x: ∏ i R_i и доказательство того, что почти по всем i x_i ∈ A_i, в элемент ограниченного произведения.

LaTeX

$$$\\mathrm{mk}(x, hx) \in \\mathrm{RestrictedProduct}(R_i, A_i, 𝓕).$$$

Lean4

/-- Constructor for `RestrictedProduct`. -/
abbrev mk (x : Π i, R i) (hx : ∀ᶠ i in 𝓕, x i ∈ A i) : Πʳ i, [R i, A i]_[𝓕] :=
  ⟨x, hx⟩

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