sym2_mono

Mathlib.Data.Finset.Sym

URI: https://scilib.ai/kg/mathlib#Finset.sym2_mono

← MathLib Explorer

English

If s ⊆ t then s.sym2 ⊆ t.sym2.

Русский

Если s ⊆ t, то s.sym2 ⊆ t.sym2.

LaTeX

$$s ⊆ t → s.sym2 ⊆ t.sym2$$

Lean4

@[simp, mono]
theorem sym2_mono (h : s ⊆ t) : s.sym2 ⊆ t.sym2 :=
  by
  rw [← val_le_iff, sym2_val, sym2_val]
  apply Multiset.sym2_mono
  rwa [val_le_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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