map — Mathlib

English

Given data of constructible set s, map it along φ to obtain data for S.

Русский

Задаем отображение данных конструктивного множества вдоль φ.

LaTeX

$$ConstructibleSetData.map φ s := s.image (BasicConstructibleSetData.map φ)$$

Lean4

/-- Given the data of the constructible set `s`, build the data of the constructible set
`{I | {x | f x ∈ I} ∈ s}`. -/
noncomputable def map (φ : R →+* S) (s : ConstructibleSetData R) : ConstructibleSetData S :=
  s.image (.map φ)

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