sumLiftRelInl — Mathlib

English

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

Русский

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

LaTeX

$$$\forall a_1,a_2.\ r(a_1,a_2) \iff \text{Sum.LiftRel } r s\, (\text{Sum.inl } a_1) (\text{Sum.inl } a_2)$$$

Lean4

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

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