union — Mathlib

English

If f is bijective on s1→t1 and on s2→t2 and f is injective on the union s1 ∪ s2, then f is bijective on the union s1 ∪ s2 to t1 ∪ t2.

Русский

Если f биекция на s1→t1 и на s2→t2 и f инъективна на s1 ∪ s2, тогда f биекция на s1 ∪ s2 → t1 ∪ t2.

LaTeX

$$$\\text{BijOn}(f,s_1,t_1)\\land\\text{BijOn}(f,s_2,t_2)\\land\\text{InjOn}(f,(s_1\\cup s_2))\\Rightarrow\\text{BijOn}(f,(s_1\\cup s_2),(t_1\\cup t_2))$$$

Lean4

theorem union (h₁ : BijOn f s₁ t₁) (h₂ : BijOn f s₂ t₂) (h : InjOn f (s₁ ∪ s₂)) : BijOn f (s₁ ∪ s₂) (t₁ ∪ t₂) :=
  ⟨h₁.mapsTo.union_union h₂.mapsTo, h, h₁.surjOn.union_union h₂.surjOn⟩

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