union

Mathlib.Topology.GDelta.Basic

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

← MathLib Explorer

English

The union of two meagre sets is meagre.

Русский

Объединение двух множеств мезгрей также является мезгре.

LaTeX

$$IsMeagre(s) \land IsMeagre(t) \rightarrow IsMeagre(s \cup t)$$

Lean4

/-- A union of two meagre sets is meagre. -/
theorem union {s t : Set X} (hs : IsMeagre s) (ht : IsMeagre t) : IsMeagre (s ∪ t) :=
  by
  rw [IsMeagre, compl_union]
  exact inter_mem hs ht

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

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

Разделы

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

Аффилиация

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