sumLexInr — Mathlib

English

Sum.inr is a relation embedding from s into Sum.Lex r s; for all a,b we have Sum.Lex r s (Sum.inr a) (Sum.inr b) iff s a b.

Русский

Sum.inr — вложение по отношению от s к Sum.Lex r s; для всех a,b выполняется Sum.Lex r s (Sum.inr a) (Sum.inr b) ⇔ s a b.

LaTeX

$$$$ Sum.inr : s \\hookrightarrow_r Sum.Lex r s \\, \\text{ и } \\forall a,b,\\; Sum.Lex r s (Sum.inr a) (Sum.inr b) \\iff s\\,a\\,b. $$$$

Lean4

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

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