liftRel_of_mem — Mathlib

English

From a ∈ ca, b ∈ cb, and R a b, LiftRel R ca cb holds.

Русский

Из a ∈ ca, b ∈ cb и R a b следует LiftRel R ca cb.

LaTeX

$$$(a\\in ca)\\land (b\\in cb)\\land R\\ a\\ b \\implies \\mathrm{LiftRel}\\,R\\ ca\\ cb$$$

Lean4

theorem liftRel_of_mem {R : α → β → Prop} {a b ca cb} (ma : a ∈ ca) (mb : b ∈ cb) (ab : R a b) : LiftRel R ca cb :=
  ⟨fun {a'} ma' => by rw [mem_unique ma' ma]; exact ⟨b, mb, ab⟩, fun {b'} mb' => by rw [mem_unique mb' mb];
    exact ⟨a, ma, ab⟩⟩

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