mono_comp — Mathlib

English

If r is directed and rb is monotone with respect to r via g, then the composition g ∘ f is directed with respect to rb.

Русский

Если r направлено и rb монотонно относительно r через g, то композиция g ∘ f направлена относительно rb.

LaTeX

$$$Directed r f \\to (\\\\forall {x y}, r x y \\to rb (g x) (g y)) \\to Directed rb (Function.comp g f)$$$

Lean4

theorem mono_comp (r : α → α → Prop) {ι} {rb : β → β → Prop} {g : α → β} {f : ι → α}
    (hg : ∀ ⦃x y⦄, r x y → rb (g x) (g y)) (hf : Directed r f) : Directed rb (g ∘ f) :=
  directed_comp.2 <| hf.mono hg

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