lift₂Expand_of — Mathlib

English

When the arguments are given by canonical representatives r₁/s₁ and r₂/s₂, the lift₂Expand equals the original predicate P evaluated at those representatives.

Русский

Если аргументы заданы каноническими представителями r₁/s₁ и r₂/s₂, то lift₂Expand равен исходному P на этих представителях.

LaTeX

$$lift_{2}^{\\mathrm{Expand}}P(hP)(r_1/s_1)(r_2/s_2) = P(r_1,s_1,r_2,s_2)$$

Lean4

@[to_additive (attr := simp)]
theorem lift₂Expand_of {C : Sort*} {P : X → S → X → S → C}
    {hP :
      ∀ (r₁ : X) (t₁ : R) (s₁ : S) (ht₁ : t₁ * s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : S) (ht₂ : t₂ * s₂ ∈ S),
        P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * s₂, ht₂⟩}
    (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) : lift₂Expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂ :=
  rfl

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