mono

Mathlib.Topology.GDelta.Basic

URI: https://scilib.ai/kg/mathlib#IsMeagre.mono

← MathLib Explorer

English

Subsets of meagre sets are meagre.

Русский

Подмножества множеств-мезгрей являются мезгрей.

LaTeX

$$IsMeagre(s) \rightarrow t \subseteq s \rightarrow IsMeagre(t)$$

Lean4

/-- Subsets of meagre sets are meagre. -/
theorem mono {s t : Set X} (hs : IsMeagre s) (hts : t ⊆ s) : IsMeagre t :=
  Filter.mem_of_superset hs (compl_subset_compl.mpr hts)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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