mem_range_of_rel — Mathlib

English

If s b (f a) holds for some a,b, then b is in the range of the underlying function of f.

Русский

Если существует a такой, что s b (f a), то b принадлежит диапазону функции f.

LaTeX

$$$\\\\forall f \\\\in r \\\\preccurlyeq_i s, \\\\forall a \\\\forall b, s b (f a) \\\\Rightarrow b \\\\in \\\\mathrm{range}(f).$$$

Lean4

theorem mem_range_of_rel (f : r ≼i s) {a : α} {b : β} : s b (f a) → b ∈ Set.range f :=
  f.mem_range_of_rel' _ _

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