English
If s is an IsDynCoverOf T F U n and t is an IsDynCoverOf T G U n, then (F ∪ G) is IsDynCoverOf T with relation U and witness s ∪ t.
Русский
Если s является IsDynCoverOf для F и U, n, и t для G и U, то F ∪ G образует динамическое покрытие также с U и объединением степеней s ∪ t.
LaTeX
$$$\big( \mathrm{IsDynCoverOf}(T, F, U, n, s) \big) \land \big( \mathrm{IsDynCoverOf}(T, G, U, n, t) \big) \Rightarrow \mathrm{IsDynCoverOf}(T, F \cup G, U, n, s \cup t)$$$
Lean4
theorem union {T : X → X} {F G : Set X} {U : Set (X × X)} {n : ℕ} {s t : Set X} (hs : IsDynCoverOf T F U n s)
(ht : IsDynCoverOf T G U n t) : IsDynCoverOf T (F ∪ G) U n (s ∪ t) :=
union_subset (hs.trans (biUnion_subset_biUnion_left subset_union_left))
(ht.trans (biUnion_subset_biUnion_left subset_union_right))
