le_iff_le — Mathlib

English

For f: α ≤i β, we have f(a) ≤ f(a') if and only if a ≤ a', i.e., f preserves and reflects the order.

Русский

Для f: α ≤i β верно, что f(a) ≤ f(a') тогда и только тогда, когда a ≤ a', то есть f сохраняет и отражает порядок.

LaTeX

$$$f(a) \le f(a') \iff a \le a'$$$

Lean4

@[simp]
theorem le_iff_le [PartialOrder α] (f : α ≤i β) : f a ≤ f a' ↔ a ≤ a' :=
  f.toOrderEmbedding.le_iff_le

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