sort_insert — Mathlib

English

If a is not in s and a is ordered relative to all b in s by r, then sorting the insert of a into s places a at the front: sort r (insert a s) = a :: sort r s.

Русский

Если a не принадлежит s и a по порядку относительно всех элементов s согласно r, то сортировка вставки a в s помещает a в начало: sort r (insert a s) = a :: sort r s.

LaTeX

$$$ \\operatorname{sort}_r(\\operatorname{insert} a\\, s) = a :: \\operatorname{sort}_r s $$$

Lean4

theorem sort_insert [DecidableEq α] {a : α} {s : Finset α} (h₁ : ∀ b ∈ s, r a b) (h₂ : a ∉ s) :
    sort r (insert a s) = a :: sort r s := by rw [← cons_eq_insert _ _ h₂, sort_cons r h₁]

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