mem_range_of_rel — Mathlib

English

If s is transitive and certain top-related ordering holds, then b lies in the image of f.

Русский

При транситивности s и определённых условий топа, элемент b принадлежит образу f.

LaTeX

$$$[IsTrans\\,\\beta\\, s]\\ (f:\\ r \\prec_i s)\\ Rightarrow (s b (f.top) \\Rightarrow b \\in \\mathrm{range}(f))$$$

Lean4

theorem mem_range_of_rel [IsTrans β s] (f : r ≺i s) {a : α} {b : β} (h : s b (f a)) : b ∈ Set.range f :=
  f.mem_range_of_rel_top <| _root_.trans h <| f.lt_top _

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