union_mem_union

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.union_mem_union

← MathLib Explorer

English

If ma ∈ a and mb ∈ b, then ma ∪ mb ∈ a ∪ b.

Русский

Если ma ∈ a и mb ∈ b, тогда ma ∪ mb ∈ a ∪ b.

LaTeX

$$$$ \forall a,b \in \mathrm{Part}(\alpha),\ \forall ma,mb \in \alpha,\ (ma \in a) \Rightarrow (mb \in b) \Rightarrow (ma \cup mb) \in (a \cup b). $$$$

Lean4

theorem union_mem_union [Union α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma ∪ mb ∈ a ∪ b := by
  simp [union_def]; aesop

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

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

Разделы

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

Аффилиация

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