union — Mathlib

English

If HasMFDerivWithinAt holds for s and for t, then it holds for s ∪ t.

Русский

Если существует MF-производная внутри s и внутри t, то существует внутри объединения s ∪ t.

LaTeX

$$$ HasMFDerivWithinAt I I' f s x f' \to HasMFDerivWithinAt I I' f t x f' \to HasMFDerivWithinAt I I' f (s \cup t) x f' $$$

Lean4

theorem union (hs : HasMFDerivWithinAt I I' f s x f') (ht : HasMFDerivWithinAt I I' f t x f') :
    HasMFDerivWithinAt I I' f (s ∪ t) x f' := by
  constructor
  · exact ContinuousWithinAt.union hs.1 ht.1
  · convert HasFDerivWithinAt.union hs.2 ht.2 using 1
    simp only [union_inter_distrib_right, preimage_union]

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