map — Mathlib

English

The map of a basic constructible set data under the identity ring homomorphism yields the same data.

Русский

Отображение данных базового конструктивного множества по тождественному гомоморфизму кольца возвращает те же данные.

LaTeX

$$∀ C, (C.map (RingHom.id R)) = C$$

Lean4

/-- Given the data of the constructible set `s`, build the data of the constructible set
`{I | {x | φ x ∈ I} ∈ s}`. -/
@[simps]
noncomputable def map (φ : R →+* S) (C : BasicConstructibleSetData R) : BasicConstructibleSetData S
    where
  f := φ C.f
  n := C.n
  g := φ ∘ C.g

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