map_inv_lt_map_inv_iff

Mathlib.Order.Hom.Basic

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

English

A second copy of the same relation: EquivLike.inv f b < EquivLike.inv f a iff b < a.

Русский

Та же зависимость: EquivLike.inv f b < EquivLike.inv f a ⇔ b < a.

LaTeX

$$$\forall {f:\ F} {a:\beta} {b:\beta},\ EquivLike.inv f b < EquivLike.inv f a \iff b < a$$$

Lean4

theorem map_inv_lt_map_inv_iff (f : F) {a b : β} : EquivLike.inv f b < EquivLike.inv f a ↔ b < a := by simp

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

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

Разделы

Аффилиация

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