small_inter_of_right

Mathlib.Logic.Small.Set

URI: https://scilib.ai/kg/mathlib#small_inter_of_right

English

The intersection s ∩ t is small if t is small.

Русский

Пересечение s ∩ t мало, если t мало.

LaTeX

$$$\operatorname{Small}(t) \Rightarrow \operatorname{Small}(s \cap t)$$$

Lean4

instance small_inter_of_right (s t : Set α) [Small.{u} t] : Small.{u} (s ∩ t : Set α) :=
  small_subset Set.inter_subset_right

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

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

Разделы

Аффилиация

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