English
RelEmbedding gives that Prod.map induces a relation embedding between Prod.Lex relations; the map takes pairs of RelEmbeddings to a RelEmbedding between Prod.Lex relations.
Русский
Из вложения RelEmbedding следует, что Prod.map порождает вложение по отношению между Prod.Lex-отношениями; отображение принимает пары вложений в Prod.Lex.
LaTeX
$$$$ \\text{prodLexMap} (f : r \\hookrightarrow_r s) (g : t \\hookrightarrow_r u) : Prod.Lex r t \\hookrightarrow_r Prod.Lex s u, \\; \\forall p,q, \\; Prod.Lex s u (Prod.map (f) (g) p) (Prod.map (f) (g) q) \\iff Prod.Lex r t p q. $$$$
Lean4
@[simp]
theorem coe_fn_mk (f : α ≃ β) (o : ∀ ⦃a b⦄, s (f a) (f b) ↔ r a b) : (RelIso.mk f @o : α → β) = f :=
rfl
