map_mono — Mathlib

English

If r x y implies s x y, then Map r f g x y implies Map s f g x y.

Русский

Если r x y ⇒ s x y, то Map r f g x y ⇒ Map s f g x y.

LaTeX

$$$\forall x y,\; \mathrm{Map}(r,f,g)\,x\,y \Rightarrow \mathrm{Map}(s,f,g)\,x\,y$$$

Lean4

theorem map_mono {r s : α → β → Prop} {f : α → γ} {g : β → δ} (h : ∀ x y, r x y → s x y) :
    ∀ x y, Relation.Map r f g x y → Relation.Map s f g x y := fun _ _ ⟨x, y, hxy, hx, hy⟩ => ⟨x, y, h _ _ hxy, hx, hy⟩

Похожие утверждения