English
Prod.map serves as a relation embedding between Prod.Lex relations; it maps a pair of relation embeddings into a relation embedding between the corresponding Lex relations.
Русский
Prod.map выступает как вложение по отношению между Prod.Lex-relations; отображает пару отображений по отношению в вложение между соответствующими Lex-relations.
LaTeX
$$$$ \\text{prodLexMap} (f,g) : Prod.Lex r t \\hookrightarrow_r Prod.Lex s u, \\quad \\forall p,q,\\; Prod.Lex r t \\; p\\; q \\iff Prod.Lex s u (Prod.map f g\\, p) (Prod.map f g\\, q). $$$$
Lean4
/-- `Prod.map` as a relation embedding. -/
@[simps]
def prodLexMap (f : r ↪r s) (g : t ↪r u) : Prod.Lex r t ↪r Prod.Lex s u
where
toFun := Prod.map f g
inj' := f.injective.prodMap g.injective
map_rel_iff' := by simp [Prod.lex_def, f.map_rel_iff, g.map_rel_iff, f.inj]
