le_inter_iff

Mathlib.Data.Multiset.UnionInter

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

English

For multisets s, t, u, we have s ≤ t ∩ u if and only if s ≤ t and s ≤ u.

Русский

Для мультимножества s, t, u верно: s ≤ t ∩ u ⇔ s ≤ t и s ≤ u.

LaTeX

$$$s \\le t \\cap u \\iff (s \\le t) \\land (s \\le u).$$$

Lean4

@[simp]
theorem le_inter_iff : s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u :=
  le_inf_iff

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

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

Разделы

Аффилиация

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