directed — Mathlib

English

If a family a is directed with respect to r, then applying a RelHom f yields a directed family with respect to s: Directed r a → Directed s (f ∘ a).

Русский

Если семейство a направлено относительно r, то применение RelHom даёт направленность относительно s: Directed r a → Directed s (f ∘ a).

LaTeX

$$$$ Directed\ r\ a \rightarrow Directed\ s\ (f \circ a). $$$$

Lean4

theorem directed [FunLike F α β] [RelHomClass F r s] {ι : Sort*} {a : ι → α} {f : F} (ha : Directed r a) :
    Directed s (f ∘ a) :=
  ha.mono_comp _ fun _ _ h ↦ map_rel f h

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