mono_comp — Mathlib

English

If r → rb monotone via g and s is DirectedOn r, then image g s is DirectedOn rb.

Русский

Если r направлено в rb через g и s направлено относительно r, то образ g s направлен относительно rb.

LaTeX

$$$DirectedOn\\ r\\ s \\to (\\\\forall {a} {b}, r a b \\to rb (g a) (g b)) \\to DirectedOn\\ rb (Set.image g s)$$$

Lean4

theorem mono_comp {r : α → α → Prop} {rb : β → β → Prop} {g : α → β} {s : Set α} (hg : ∀ ⦃x y⦄, r x y → rb (g x) (g y))
    (hf : DirectedOn r s) : DirectedOn rb (g '' s) :=
  directedOn_image.mpr (hf.mono hg)

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