mem_sort

Mathlib.Data.Multiset.Sort

URI: https://scilib.ai/kg/mathlib#Multiset.mem_sort

English

For all s and a, a is in sort r s iff a is in s.

Русский

Для любых s и a, a принадлежит sort r s тогда и только тогда, когда a принадлежит s.

LaTeX

$$$$ a \\in \\operatorname{sort} r s \\iff a \\in s $$$$

Lean4

@[simp]
theorem mem_sort {s : Multiset α} {a : α} : a ∈ sort r s ↔ a ∈ s := by rw [← mem_coe, sort_eq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru