rel_of_liftRel — Mathlib

English

If ca and cb are related by LiftRel R, then every a in ca and every b in cb satisfy R a b.

Русский

Если ca и cb связаны LiftRel R, то для каждого a∈ca и каждого b∈cb имеет R a b.

LaTeX

$$$\\mathrm{LiftRel}\\,R\\ ca\\ cb \\Rightarrow \\forall a\\in ca\\,\\forall b\\in cb,\\ R\\ a\\ b$$$

Lean4

theorem rel_of_liftRel {R : α → β → Prop} {ca cb} : LiftRel R ca cb → ∀ {a b}, a ∈ ca → b ∈ cb → R a b
  | ⟨l, _⟩, a, b, ma, mb => by
    let ⟨b', mb', ab'⟩ := l ma
    rw [mem_unique mb mb']; exact ab'

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