surjOn — Mathlib

English

Let f be a principal segment embedding f: r ≺i s. Then f is surjective onto the subset {b in β | s b f.top}; equivalently, for every b with s b f.top there exists a with f a = b.

Русский

Пусть f — вложение PrincipalSeg f: r ≺i s. Тогда отображение f образует сюръекцию на подмножество {b ∈ β | s b f.top}; эквивалентно: для каждого b с условием s b f.top существует a ∈ α такой что f(a) = b.

LaTeX

$$$Set.SurjOn\ f\ Set.univ\ \{ b \mid s\ b\ f.top \}$$$

Lean4

theorem surjOn (f : r ≺i s) : Set.SurjOn f Set.univ {b | s b f.top} :=
  by
  intro b h
  simpa using mem_range_of_rel_top _ h

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