cons_lt_cons_iff — Mathlib

English

Inserting the same element preserves strict order: insert(a, s) < insert(a, t) iff s < t.

Русский

Добавление одинакового элемента сохраняет строгость порядка: insert(a, s) < insert(a, t) тогда и только тогда, когда s < t.

LaTeX

$$$insert(a, s) < insert(a, t) \iff s < t$$$

Lean4

@[simp]
theorem cons_lt_cons_iff : a ::ₘ s < a ::ₘ t ↔ s < t :=
  lt_iff_lt_of_le_iff_le' (cons_le_cons_iff _) (cons_le_cons_iff _)

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