sort_cons — Mathlib

English

For any Finset s and element a, a ∈ sort_r s iff a ∈ s.

Русский

Для любого Finset s и элемента a выполняется a ∈ sort_r s тогда и только тогда, когда a ∈ s.

LaTeX

$$$ a \\in \\operatorname{sort}_r(s) \\iff a \\in s $$$

Lean4

theorem sort_cons {a : α} {s : Finset α} (h₁ : ∀ b ∈ s, r a b) (h₂ : a ∉ s) : sort r (cons a s h₂) = a :: sort r s := by
  rw [sort, cons_val, Multiset.sort_cons r a _ h₁, sort_val]

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