liftPred_coe — Mathlib

English

For a germ f, LiftPred p (f) is equivalent to supplanting f by its representative: the equivalence holds by rfl.

Русский

Для жермы f LiftPred p(f) эквивалентно предикату на представителе: эквивалентность тривиальна.

LaTeX

$$$ \\mathrm{LiftPred} p (f) \\iff \\forall^\\infty x\\in l, p(f(x)) $$$

Lean4

@[simp]
theorem liftPred_coe {p : β → Prop} {f : α → β} : LiftPred p (f : Germ l β) ↔ ∀ᶠ x in l, p (f x) :=
  Iff.rfl

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