liftPred_const_iff

Mathlib.Order.Filter.Germ.Basic

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

English

If l is nonempty, LiftPred p (↑x) is equivalent to p(x).

Русский

Если l непуст, LiftPred p (↑x) эквивалентно p(x).

LaTeX

$$$ \\mathrm{LiftPred}\\, p (\\uparrow x) \\iff p x $$$

Lean4

@[simp]
theorem liftPred_const_iff [NeBot l] {p : β → Prop} {x : β} : LiftPred p (↑x : Germ l β) ↔ p x :=
  @eventually_const _ _ _ (p x)

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

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

Разделы

Аффилиация

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