lt_iff_lt — Mathlib

English

For aStrictMonoOn function on a set, a < b is equivalent to f a < f b for elements of the set.

Русский

Для StrictMonoOn на множестве a < b эквивалентно f(a) < f(b) для элементов множества.

LaTeX

$$$hf : StrictMonoOn f s \\Rightarrow ∀ {a b}, a ∈ s → b ∈ s → f a < f b ↔ a < b$$$

Lean4

theorem lt_iff_lt (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a < f b ↔ a < b := by
  rw [lt_iff_le_not_ge, lt_iff_le_not_ge, hf.le_iff_le ha hb, hf.le_iff_le hb ha]

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