le_ndinter

Mathlib.Data.Multiset.FinsetOps

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

English

For multisets s,t,u, s ≤ ndinter t u is equivalent to s ≤ t and s ⊆ u.

Русский

Для мультимножест s,t,u: s ≤ ndinter t u эквивалентно s ≤ t и s ⊆ u.

LaTeX

$$$\\mathrm{s} \\leq \\mathrm{ndinter}(t,u) \\iff \\mathrm{s} \\leq t \\land \\mathrm{s} \\subseteq u$$$

Lean4

theorem le_ndinter {s t u : Multiset α} : s ≤ ndinter t u ↔ s ≤ t ∧ s ⊆ u := by simp [ndinter, le_filter, subset_iff]

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

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

Разделы

Аффилиация

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