mem_range_of_rel_top — Mathlib

English

If f.top belongs to a specified set p, then the top-related condition describes membership of the image of f restricted to p.

Русский

Если верхний элемент f.top принадлежит заданному множеству p, то условие принадлежности образа f ограниченного множеством p описывает изображение f.

LaTeX

$$$\\forall f:\\ r \\prec_i s,\\ f.top\\in p \\Rightarrow b \\in \\mathrm{range}(f)$; (precise formulation in context of codRestrict).$$

Lean4

theorem mem_range_of_rel_top (f : r ≺i s) {b : β} (h : s b f.top) : b ∈ Set.range f :=
  f.mem_range_iff_rel.2 h

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