symm_apply_le

Mathlib.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#OrderIso.symm_apply_le

English

For e, x ≤ e.symm y iff y ≥ e x.

Русский

Для e: x ≤ e.symm(y) тогда и только если y ≥ e(x).

LaTeX

$$$ x \le e.symm y \iff y \ge e x $$$

Lean4

theorem symm_apply_le (e : α ≃o β) {x : α} {y : β} : e.symm y ≤ x ↔ y ≤ e x :=
  e.symm_apply_rel

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

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

Разделы

Аффилиация

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