English
Sum.inl is a relation embedding from r into Sum.Lex r s; in particular, for all a,b we have Sum.Lex r s (Sum.inl a) (Sum.inl b) iff r a b.
Русский
Sum.inl — вложение по отношению от r к Sum.Lex r s; для всех a,b выполняется равенство Sum.Lex r s (Sum.inl a) (Sum.inl b) ⇔ r a b.
LaTeX
$$$$ Sum.inl : r \\hookrightarrow_r Sum.Lex r s \\, \\text{ и } \\forall a,b,\\; Sum.Lex r s (Sum.inl a) (Sum.inl b) \\iff r\\,a\\,b. $$$$
Lean4
/-- `Sum.inl` as a relation embedding into `Sum.Lex r s`. -/
@[simps]
def sumLexInl (r : α → α → Prop) (s : β → β → Prop) : r ↪r Sum.Lex r s
where
toFun := Sum.inl
inj' := Sum.inl_injective
map_rel_iff' := Sum.lex_inl_inl
