inter_univ

Mathlib.Data.Finset.BooleanAlgebra

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

English

The intersection with the universal set yields the original set: s ∩ univ = s.

Русский

Пересечение с универcумом даёт исходное множество: s ∩ univ = s.

LaTeX

$$$ s \\cap univ = s $$$

Lean4

@[simp]
theorem inter_univ (s : Finset α) : s ∩ univ = s := by rw [inter_comm, univ_inter]

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

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

Разделы

Аффилиация

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