liftExpand_of — Mathlib

English

The lifted function agrees with the original on representatives in the localization.

Русский

Поднятая функция совпадает с исходной на представителях в локализации.

LaTeX

$$liftExpand_of {P} {hP} (r) (s) : liftExpand P hP (r /ₒ s) = P r s$$

Lean4

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

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