English
Sum.map acts as a relation embedding between Sum.Lex relations: Sum.Lex r t is embedded into Sum.Lex s u via Sum.map f g.
Русский
Sum.map действует как вложение по отношению между Sum.Lex: Sum.Lex r t встроено в Sum.Lex s u через Sum.map f g.
LaTeX
$$$$ Sum.map(f,g) : Sum.Lex r t \\hookrightarrow_r Sum.Lex s u, \\quad \\forall x,y,\\; Sum.Lex r t x y \\iff Sum.Lex s u (Sum.map f g \\, x) (Sum.map f g \\, y). $$$$
Lean4
/-- `Sum.map` as a relation embedding between `Sum.Lex` relations. -/
@[simps]
def sumLexMap (f : r ↪r s) (g : t ↪r u) : Sum.Lex r t ↪r Sum.Lex s u
where
toFun := Sum.map f g
inj' := f.injective.sumMap g.injective
map_rel_iff' := by rintro (a | b) (c | d) <;> simp [f.map_rel_iff, g.map_rel_iff]
