singleton_inter

Mathlib.Data.Set.Subsingleton

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

English

The intersection of {a} with s is subsingleton.

Русский

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

LaTeX

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

Lean4

theorem singleton_inter : ({ a } ∩ s).Subsingleton :=
  Set.subsingleton_of_subset_singleton Set.inter_subset_left

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

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

Разделы

Аффилиация

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