LiftPred — Mathlib

English

LiftPred p maps a germ to the proposition that p holds for its representative almost everywhere with respect to l.

Русский

LiftPred p переводит предикат на жермы так, что выполняется, что p относится к представителю почти повсюду относительно l.

LaTeX

$$$ \\mathrm{LiftPred}\\, p\\; (f) \\;:=\\; \\text{liftOn } f\\; (\\lambda f. \\forall^\\infty x\\in l, p(f(x))) \\text{ ... }$$$

Lean4

/-- Lift a predicate on `β` to `Germ l β`. -/
def LiftPred (p : β → Prop) (f : Germ l β) : Prop :=
  liftOn f (fun f => ∀ᶠ x in l, p (f x)) fun _f _g H => propext <| eventually_congr <| H.mono fun _x hx => hx ▸ Iff.rfl

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