image — Mathlib

English

The image of a set s under a relation R is the set of all b such that there exists a ∈ s with a ~[R] b.

Русский

Образ множества s по отношению R — это множество всех b, для которых существует a ∈ s такое что a связано с b отношением R.

LaTeX

$$R.image\,s = { b ∈ β \mid ∃ a ∈ s, a ~[R] b }$$

Lean4

/-- Image of a set under a relation. -/
def image : Set β :=
  {b | ∃ a ∈ s, a ~[R] b}

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