map_rel

Mathlib.ModelTheory.Basic

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Embedding.map_rel

English

If φ: M ↪[L] N, then RelMap r x → RelMap r (φ ∘ x) for any relation symbol r.

Русский

Если φ: M ↪[L] N, то RelMap r x → RelMap r (φ ∘ x) для любого отношения r.

LaTeX

$$$\\RelMap r\\ x \\Rightarrow \\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 :=
  StrongHomClass.map_rel φ r x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru