English
If s Rel r t and a mapping h registers that p a b holds whenever r a b, then Rel p s t holds.
Русский
Если s связано с t по отношению r и существует правило h, которое сохраняет отношение p по мере того, как r держит соответствие между элементами, тогда Rel p s t верно.
LaTeX
$$$Rel\ r\ s\ t \rightarrow (\forall a \in s, \forall b \in t, r\ a\ b \rightarrow p\ a\ b) \rightarrow Rel\ p\ s\ t$$$
Lean4
theorem mono {r p : α → β → Prop} {s t} (hst : Rel r s t) (h : ∀ a ∈ s, ∀ b ∈ t, r a b → p a b) : Rel p s t := by
induction hst with
| zero => exact Rel.zero
| @cons a b s t hab _hst
ih =>
apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'
