tprod_congr_subtype — Mathlib

English

If P x ↔ Q x for all x, then the tprod over the subtype {x | P x} of f x equals the tprod over {x | Q x} of f x.

Русский

Если P x эквивалентно Q x для каждого x, то тпроизведение по подтипам совпадает.

LaTeX

$$∏' x : { x // P x }, f x = ∏' x : { x // Q x }, f x$$

Lean4

@[to_additive]
theorem tprod_congr_subtype (f : β → α) {P Q : β → Prop} (h : ∀ x, P x ↔ Q x) :
    ∏' x : { x // P x }, f x = ∏' x : { x // Q x }, f x :=
  tprod_congr_set_coe f <| Set.ext h

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