derivedSet_union — Mathlib

English

derivedSet(A ∪ B) = derivedSet(A) ∪ derivedSet(B).

Русский

Производное множества от объединения равно объединению производных: \operatorname{derivedSet}(A \cup B) = \operatorname{derivedSet}(A) \cup \operatorname{derivedSet}(B).

LaTeX

$$$$\operatorname{derivedSet}(A \cup B) = \operatorname{derivedSet}(A) \cup \operatorname{derivedSet}(B).$$$$

Lean4

theorem derivedSet_union (A B : Set X) : derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B :=
  by
  ext x
  simp [derivedSet, ← sup_principal, accPt_sup]

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