fromSum_bijective — Mathlib

English

Same as FromSum Bijective, reaffirming the bijection for AreComplementary embeddings.

Русский

То же самое, что и FromSum Bijective, подтверждающее биекцию для взаимодополняющих вложений.

LaTeX

$$AreComplementary.fromSum e1 e2 is bijective$$

Lean4

theorem fromSum_bijective : Function.Bijective (fromSum e₁ e₂) :=
  by
  constructor
  · rintro (i₁ | i₂) (j₁ | j₂) h
    · obtain rfl := e₁.injective_f h
      rfl
    · exact (ac.disjoint _ _ h).elim
    · exact (ac.disjoint _ _ h.symm).elim
    · obtain rfl := e₂.injective_f h
      rfl
  · intro n
    obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union n
    · exact ⟨Sum.inl i₁, rfl⟩
    · exact ⟨Sum.inr i₂, rfl⟩

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