map_rel_iff

Mathlib.Order.InitialSeg

URI: https://scilib.ai/kg/mathlib#InitialSeg.map_rel_iff

English

For any a,b, s (f a) (f b) if and only if r a b.

Русский

Для любых a,b верно, что s (f a) (f b) эквивалентно r a b.

LaTeX

$$$\\\\forall a,b, \\\\ s (f a) (f b) \\\\iff \\\\ r a b.$$$

Lean4

theorem map_rel_iff {a b : α} (f : r ≼i s) : s (f a) (f b) ↔ r a b :=
  f.map_rel_iff'

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

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

Разделы

Аффилиация

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