inter_subset_right

Mathlib.Data.List.Lattice

URI: https://scilib.ai/kg/mathlib#List.inter_subset_right

English

l1 ∩ l2 is a subset of l2.

Русский

Пересечение l1 и l2 является подмножеством l2.

LaTeX

$$$\\forall {\\\\alpha} [\\\\mathrm{DecidableEq} \\\\alpha] {l_1 l_2 : List \\\\alpha}, (l_1 \\\\cap l_2) \\\\subseteq l_2$$$

Lean4

theorem inter_subset_right {l₁ l₂ : List α} : l₁ ∩ l₂ ⊆ l₂ := fun _ => mem_of_mem_inter_right

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

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

Разделы

Аффилиация

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