small_sep

Mathlib.Logic.Small.Set

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

English

The subset {x in s | P(x)} is small whenever s is small.

Русский

Подмножество {x ∈ s | P(x)} малое, если s малое.

LaTeX

$$$\operatorname{Small}(s) \Rightarrow \operatorname{Small}\{ x \in s \mid P(x) \}$$$

Lean4

instance small_sep (s : Set α) (P : α → Prop) [Small.{u} s] : Small.{u} {x | x ∈ s ∧ P x} :=
  small_subset (Set.sep_subset s P)

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

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

Разделы

Аффилиация

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