sumLiftRelInr — Mathlib

English

The function Sum.inr is an embedding of s into Sum.LiftRel r s.

Русский

Функция Sum.inr является вложением s в Sum.LiftRel r s.

LaTeX

$$$\forall b_1,b_2.\ s(b_1,b_2) \iff \text{Sum.LiftRel } r s\, (\text{Sum.inr } b_1) (\text{Sum.inr } b_2)$$$

Lean4

/-- `Sum.inr` as a relation embedding into `Sum.LiftRel r s`. -/
@[simps]
def sumLiftRelInr (r : α → α → Prop) (s : β → β → Prop) : s ↪r Sum.LiftRel r s
    where
  toFun := Sum.inr
  inj' := Sum.inr_injective
  map_rel_iff' := Sum.liftRel_inr_inr

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