inter_singleton

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.Subsingleton.inter_singleton

English

The intersection of a set s with the singleton {a} is subsingleton.

Русский

Пересечение множества s с множесвом {a} является субоднозначным.

LaTeX

$$$ (s \cap { a }).Subsingleton $$$

Lean4

theorem inter_singleton : (s ∩ { a }).Subsingleton :=
  Set.subsingleton_of_subset_singleton Set.inter_subset_right

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

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

Разделы

Аффилиация

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