English
If p respects r (hrp), then EqvGen r a b implies EqvGen p a b. In particular, EqvGen is monotone with respect to implication along r.
Русский
Если p сохраняет отношение r (hrp), то если a и b эквивалентны по r, то a и b эквиваленты по p.
LaTeX
$$(∀ a b, r a b ⇒ p a b) ⇒ (\\\\operatorname{EqvGen} r a b ⇒ \\\\operatorname{EqvGen} p a b)$$
Lean4
theorem mono {r p : α → α → Prop} (hrp : ∀ a b, r a b → p a b) (h : EqvGen r a b) : EqvGen p a b := by
induction h with
| rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
| refl => exact EqvGen.refl _
| symm a b _ ih => exact EqvGen.symm _ _ ih
| trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
