LiftPPreservation — Mathlib

English

LiftP is preserved when moving from an element x to its abs x: LiftP p (abs x) iff LiftP p x.

Русский

LiftP сохраняется при переходе от элемента x к его абс-образу: LiftP p (abs x) эквивалентно LiftP p x.

LaTeX

$$$$ \\forall \\alpha\\ p\\;\\forall x,\\ LiftP\\ p\\ (\\mathrm{abs}\\ x) \\iff \\ LiftP\\ p\\ x. $$$$

Lean4

/-- does `abs` preserve `liftp`? -/
def LiftPPreservation : Prop :=
  ∀ ⦃α : TypeVec n⦄ (p : ∀ ⦃i⦄, α i → Prop) (x : q.P α), LiftP p (abs x) ↔ LiftP p x

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