English
Let f and g be relation embeddings between r ↪r s and t ↪r u. Then Sum.map f g defines a relation embedding from Sum.LiftRel r t to Sum.LiftRel s u.
Русский
Пусть f и g — вложения по отношению между r↪r s и t↪r u. Тогда Sum.map f g задаёт вложение по отношению между Sum.LiftRel r t и Sum.LiftRel s u.
LaTeX
$$$$ Sum.map(f,g) : Sum.LiftRel(r,t) \\hookrightarrow Sum.LiftRel(s,u). $$$$
Lean4
/-- `Sum.map` as a relation embedding between `Sum.LiftRel` relations. -/
@[simps]
def sumLiftRelMap (f : r ↪r s) (g : t ↪r u) : Sum.LiftRel r t ↪r Sum.LiftRel 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]
