tprod_univ — Mathlib

English

The tprod over the whole universe equals the tprod over the whole domain: ∏' x : Set.univ, f x = ∏' x, f x.

Русский

Т-произведение по всему множеству равно т-произведению по всей области.

LaTeX

$$$\\\\prod' x : (Set.univ : Set β), f x = \\\\prod' x, f x$$$

Lean4

@[to_additive (attr := simp)]
theorem tprod_univ (f : β → α) : ∏' x : (Set.univ : Set β), f x = ∏' x, f x :=
  tprod_subtype_eq_of_mulSupport_subset <| Set.subset_univ _

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