liftPred_const

Mathlib.Order.Filter.Germ.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Germ.liftPred_const

English

If p(x) holds, then the germ of the constant x satisfies LiftPred p.

Русский

Если p(x) верно, то жерма константы x удовлетворяет LiftPred p.

LaTeX

$$$ \\mathrm{LiftPred}\\, p (\\uparrow x) $ при условии $ p x $.$$

Lean4

theorem liftPred_const {p : β → Prop} {x : β} (hx : p x) : LiftPred p (↑x : Germ l β) :=
  Eventually.of_forall fun _y => hx

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru