map_rel

Mathlib.Order.RelIso.Basic

URI: https://scilib.ai/kg/mathlib#RelHom.map_rel

English

A RelHom f preserves the relation: r a b implies s (f a) (f b).

Русский

Отображение сохраняет отношение: если r(a,b), то s(f(a),f(b)).

LaTeX

$$$\forall {a b},\ r\ a\ b \Rightarrow s\ (f\ a)\ (f\ b)$$$

Lean4

protected theorem map_rel (f : r →r s) {a b} : r a b → s (f a) (f b) :=
  f.map_rel'

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

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

Разделы

Аффилиация

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