directedOn — Mathlib

English

If t is Directed under r, then its image under f is Directed under s: DirectedOn r t → DirectedOn s (f '' t).

Русский

Если множество t направлено относительно r, то образ under f подчиняется направленности относительно s: DirectedOn r t → DirectedOn s (f'' t).

LaTeX

$$$$ DirectedOn\ r\ t \rightarrow DirectedOn\ s\ (f''\ t). $$$$

Lean4

theorem directedOn [FunLike F α β] [RelHomClass F r s] {f : F} {t : Set α} (hs : DirectedOn r t) :
    DirectedOn s (f '' t) :=
  hs.mono_comp fun _ _ h ↦ map_rel f h

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