ndinter_eq_left

Mathlib.Data.Multiset.FinsetOps

URI: https://scilib.ai/kg/mathlib#Multiset.Subset.ndinter_eq_left

← MathLib Explorer

English

If s ⊆ t, then ndinter s t = s.

Русский

Если s ⊆ t, то ndinter s t = s.

LaTeX

$$s \subseteq t \Rightarrow ndinter s t = s$$

Lean4

theorem ndinter_eq_left {s t : Multiset α} (h : s ⊆ t) : s.ndinter t = s :=
  by
  induction s, t using Quot.induction_on₂
  rw [quot_mk_to_coe'', quot_mk_to_coe'', coe_ndinter, List.Subset.inter_eq_left h]

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

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

Разделы

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

Аффилиация

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