English
Fix an a with Not (r a a). Then the map b ↦ (a,b) embeds s into Prod.Lex r s; i.e., Prod.mk a is an embedding with respect to the lexicographic product.
Русский
Пусть выбрано a с Not(r a a). Тогда отображение b ↦ (a,b) является вложением s в Prod.Lex r s; т. е. Prod.mk a задаёт вложение по отношению.
LaTeX
$$$$ \\text{prodLexMkLeft} : s \\hookrightarrow_r Prod.Lex r s \\, (\\forall a,b), \\; \\forall a,b' \\, (Prod.Lex\\, r\\, s\\ { fst := a, snd := b } { fst := a, snd := b' }) \\iff s\\,b\\,b'. $$$$
Lean4
/-- `fun b ↦ Prod.mk a b` as a relation embedding. -/
@[simps]
def prodLexMkLeft (s : β → β → Prop) {a : α} (h : ¬r a a) : s ↪r Prod.Lex r s
where
toFun := Prod.mk a
inj' := Prod.mk_right_injective a
map_rel_iff' := by simp [Prod.lex_def, h]
