exists_of_liftRel_left

Mathlib.Data.Seq.Computation

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

English

If H is a LiftRel relation between ca and cb, then for any a ∈ ca there exists b ∈ cb with R a b.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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