map_lt_map_iff

Mathlib.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#map_lt_map_iff

English

The map f preserves strict order: f a < f b iff a < b, for an order isomorphism class F.

Русский

Отображение f сохраняет строгое порядка: f a < f b ⇔ a < b.

LaTeX

$$$\forall f:\ F,\ a,b:\alpha,\ f a < f b \iff a < b$$$

Lean4

theorem map_lt_map_iff (f : F) {a b : α} : f a < f b ↔ a < b :=
  lt_iff_lt_of_le_iff_le' (map_le_map_iff f) (map_le_map_iff f)

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

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

Разделы

Аффилиация

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