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