map_rel — Mathlib

English

If φ: M →[L] N and r is an n-ary relation, then whenever x satisfies RelMap r on M, φ ∘ x satisfies RelMap r on N.

Русский

Если φ: M →[L] N и r — отношение, то если x удовлетворяет RelMap r в M, то φ ∘ x удовлетворяет RelMap r в N.

LaTeX

$$$\\mathrm{RelMap}\\ r\\ x \\Rightarrow \\mathrm{RelMap}\\ r\\ (\\phi \\circ x)$$$

Lean4

@[simp]
theorem map_rel (φ : M →[L] N) {n : ℕ} (r : L.Relations n) (x : Fin n → M) : RelMap r x → RelMap r (φ ∘ x) :=
  HomClass.map_rel φ r x

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