binaryFanOfPropIsLimit — Mathlib

Lean4
/-- A product indexed by `I` is a binary product of the products indexed by a subset of `I` and its
complement.
-/
noncomputable def binaryFanOfPropIsLimit [∀ i, Decidable (P i)] : IsLimit (Pi.binaryFanOfProp X P) :=
  BinaryFan.isLimitMk
    (fun s ↦
      Pi.lift fun b ↦
        if h : P b then s.π.app ⟨WalkingPair.left⟩ ≫ Pi.π (fun (i : { x : I // P x }) ↦ X i.val) ⟨b, h⟩
        else s.π.app ⟨WalkingPair.right⟩ ≫ Pi.π (fun (i : { x : I // ¬P x }) ↦ X i.val) ⟨b, h⟩)
    (by aesop) (by aesop)
    (fun _ _ h₁ h₂ ↦
      Pi.hom_ext _ _ fun b ↦ by
        by_cases h : P b
        · simp [← h₁, dif_pos h]
        · simp [← h₂, dif_neg h])
Похожие утверждения