mono — Mathlib

English

If r → rb monotone under g and hf: DirectedOn r s, then DirectedOn rb (Set.image g s).

Русский

Если r перейдёт в rb через монотонное отображение g и s направлено относительно r, то image 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 {s : α → α → Prop} {ι} {f : ι → α} (H : ∀ a b, r a b → s a b) (h : Directed r f) : Directed s f :=
  fun a b =>
  let ⟨c, h₁, h₂⟩ := h a b
  ⟨c, H _ _ h₁, H _ _ h₂⟩

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