map_onRelation — Mathlib

English

If ϕ is an expansion on M, then RelMap(ϕ.onRelation R) = RelMap R.

Русский

Если ϕ расширение на M, то RelMap(ϕ.onRelation R) = RelMap R.

LaTeX

$$$\mathrm{RelMap}(\varphi.onRelation R)\; x = \mathrm{RelMap} R\; x$$$

Lean4

@[simp]
theorem map_onRelation {M : Type*} [L.Structure M] [L'.Structure M] [ϕ.IsExpansionOn M] {n} (R : L.Relations n)
    (x : Fin n → M) : RelMap (ϕ.onRelation R) x = RelMap R x :=
  IsExpansionOn.map_onRelation R x

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