liftRel_const_iff

Mathlib.Order.Filter.Germ.Basic

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

← MathLib Explorer

English

If l is nonempty, LiftRel r (↑x) (↑y) holds if and only if r x y.

Русский

Если l непуст, LiftRel r (↑x) (↑y) держится тогда и только тогда, когда r x y.

LaTeX

$$$ \\mathrm{LiftRel} r (\\uparrow x) (\\uparrow y) \\iff r x y $$$

Lean4

@[simp]
theorem liftRel_const_iff [NeBot l] {r : β → γ → Prop} {x : β} {y : γ} : LiftRel r (↑x : Germ l β) ↑y ↔ r x y :=
  @eventually_const _ _ _ (r x y)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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