small_subset

Mathlib.Logic.Small.Set

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

English

If t ⊆ s and S is Small, then t is Small.

Русский

Если t ⊆ s и s мал, то t мал.

LaTeX

$$$(t \subseteq s) \Rightarrow (Small(s) \Rightarrow Small(t)).$$$

Lean4

theorem small_subset {s t : Set α} (hts : t ⊆ s) [Small.{u} s] : Small.{u} t :=
  small_of_injective (Set.inclusion_injective hts)

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

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

Разделы

Аффилиация

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