mem_sort — Mathlib

English

For any a and Finset s, a belongs to the sorted list sort_r s iff a belongs to s.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mem_sort {s : Finset α} {a : α} : a ∈ sort r s ↔ a ∈ s :=
  Multiset.mem_sort _

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