insert_le_insert — Mathlib

English

The strict order between two conses is determined by the inserted elements: s.cons a < s.cons b iff a < b, provided a,b not in s.

Русский

Строгий порядок между двумя константами определяется вставленными элементами: s.cons a < s.cons b, если a < b, при условии a,b не принадлежат s.

LaTeX

$$$$ \\operatorname{toColex}(\\operatorname{cons} a s) < \\operatorname{toColex}(\\operatorname{cons} b s) \\iff a < b $$$$

Lean4

theorem insert_le_insert (ha : a ∉ s) (hb : b ∉ s) : toColex (insert a s) ≤ toColex (insert b s) ↔ a ≤ b := by
  rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_le_cons]

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