union_union — Mathlib

English

If f is surjective onto t1 and onto t2 from s, then it is surjective onto t1 ∪ t2 from s.

Русский

Если f для множества s за покрывает t1 и t2, тогда покрывает t1 ∪ t2.

LaTeX

$$$\\text{SurjOn } f\\ s\\ t_1 \\land \\text{SurjOn } f\\ s\\ t_2 \\Rightarrow \\text{SurjOn } f\\ s\\ (t_1 \\cup t_2).$$$

Lean4

theorem union_union (h₁ : SurjOn f s₁ t₁) (h₂ : SurjOn f s₂ t₂) : SurjOn f (s₁ ∪ s₂) (t₁ ∪ t₂) :=
  (h₁.mono subset_union_left (Subset.refl _)).union (h₂.mono subset_union_right (Subset.refl _))

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