union — Mathlib

English

If f maps s onto t1 and onto t2, then it maps s onto t1 ∪ t2.

Русский

Если f отображает s на t1 и на t2, то он отображает s на t1 ∪ t2.

LaTeX

$$$$ \\operatorname{SurjOn}(f,s,t_1) \\to \\operatorname{SurjOn}(f,s,t_2) \\to \\operatorname{SurjOn}(f,s,t_1 \\cup t_2) $$$$

Lean4

theorem union (h₁ : SurjOn f s t₁) (h₂ : SurjOn f s t₂) : SurjOn f s (t₁ ∪ t₂) := fun _ hx =>
  hx.elim (fun hx => h₁ hx) fun hx => h₂ hx

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