exists_of_liftRel_right

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.exists_of_liftRel_right

English

If H is LiftRel R ca cb and b ∈ cb, there exists a ∈ ca with R a b.

Русский

Если H = LiftRel R ca cb и b ∈ cb, то существует a ∈ ca такое, что R a b.

LaTeX

$$$\\forall b\\in cb,\\ \\exists a\\in ca,\\ R\\ a\\ b$$$

Lean4

theorem exists_of_liftRel_right {R : α → β → Prop} {ca cb} (H : LiftRel R ca cb) {b} (h : b ∈ cb) :
    ∃ a, a ∈ ca ∧ R a b :=
  H.right h

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

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

Разделы

Аффилиация

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