hasBinaryProduct_of_products — Mathlib

English

Let X be a family of objects indexed by I, and P a predicate on I. If all the required products exist, then the binary product of the product over {i : P i} and the product over {i : ¬P i} exists in the ambient category.

Русский

Пусть X_i — семейство объектов, индексированное по I, и P — свойство на I. Пусть существуют соответствующие произведения. Тогда существует двоичное произведение над двумя подсемействами: по тем i, для которых P i истина, и по тем i, для которых P i ложь.

LaTeX

$$$\mathrm{HasBinaryProduct}\Big(\prod^{\mathsf{c}}_{i:\{x:I\mid P x\}} X_i\Big)\Big(\prod^{\mathsf{c}}_{i:\{x:I\mid \neg P x\}} X_i\Big)$$$

Lean4

theorem hasBinaryProduct_of_products :
    HasBinaryProduct (∏ᶜ (fun (i : { x : I // P x }) ↦ X i.val)) (∏ᶜ (fun (i : { x : I // ¬P x }) ↦ X i.val)) := by
  classical exact ⟨Pi.binaryFanOfProp X P, Pi.binaryFanOfPropIsLimit X P⟩

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