inter_union_self

Mathlib.Data.Finset.Lattice.Basic

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

English

Let s, t be finite sets. Then s ∩ (t ∪ s) = s.

Русский

Пусть s, t — конечные множества. Тогда s ∩ (t ∪ s) = s.

LaTeX

$$$ s \cap (t \cup s) = s $$$

Lean4

@[simp]
theorem inter_union_self (s t : Finset α) : s ∩ (t ∪ s) = s := by rw [inter_comm, union_inter_cancel_right]

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

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

Разделы

Аффилиация

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