le_map_inv_iff — Mathlib

English

The inequality a ≤ inv f b is equivalent to f a ≤ b for order-homomorphisms derived from F.

Русский

Неравенство a ≤ inv f b эквивалентно f a ≤ b для отображения, полученного из F.

LaTeX

$$$\forall f:\ F,\ a:\alpha,\ b:\beta,\ a \le EquivLike.inv f b \iff f a \le b$$$

Lean4

@[simp]
theorem le_map_inv_iff (f : F) {a : α} {b : β} : a ≤ EquivLike.inv f b ↔ f a ≤ b :=
  by
  convert (map_le_map_iff f).symm
  exact (EquivLike.right_inv _ _).symm

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