preimage — Mathlib

English

The preimage of a set t under a relation R is the set of all a ∈ α such that ∃ b ∈ t with a ~[R] b.

Русский

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

LaTeX

$$R.preimage\,t = { a ∈ α \mid ∃ b ∈ t, a ~[R] b }$$

Lean4

/-- Preimage of a set `t` under a relation `R`. Same as the image of `t` under `R.inv`. -/
def preimage : Set α :=
  {a | ∃ b ∈ t, a ~[R] b}

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