Functions to "half" Sum

Here we study functions of type α → β₁ ⊕ β₂ that happen to contain image in only one of the half of its codomain.

theorem sum_ne_inl {β₁ β₂ : Type} {x : β₁ ⊕ β₂} (hx₁ : ∀ (b₁ : β₁), x ≠ ◩b₁) : ∃ (b₂ : β₂), x = ◪b₂

theorem sum_ne_inr {β₁ β₂ : Type} {x : β₁ ⊕ β₂} (hx₂ : ∀ (b₂ : β₂), x ≠ ◪b₂) : ∃ (b₁ : β₁), x = ◩b₁

theorem fn_sum_ne_inl {β₁ β₂ α : Type} {f : α → β₁ ⊕ β₂} (hf : ∀ (a : α) (b₁ : β₁), f a ≠ ◩b₁) (a : α) : ∃ (b₂ : β₂), f a = ◪b₂

theorem fn_sum_ne_inr {β₁ β₂ α : Type} {f : α → β₁ ⊕ β₂} (hf : ∀ (a : α) (b₂ : β₂), f a ≠ ◪b₂) (a : α) : ∃ (b₁ : β₁), f a = ◩b₁

noncomputable def fn_of_sum_ne_inl {β₁ β₂ α : Type} {f : α → β₁ ⊕ β₂} (hf : ∀ (a : α) (b₁ : β₁), f a ≠ ◩b₁) : α → β₂

Assume f : α → β₁ ⊕ β₂ never reaches β₁ values. We convert f to α → β₂ function.

Equations

• fn_of_sum_ne_inl hf x✝ = ⋯.choose

noncomputable def fn_of_sum_ne_inr {β₁ β₂ α : Type} {f : α → β₁ ⊕ β₂} (hf : ∀ (a : α) (b₂ : β₂), f a ≠ ◪b₂) : α → β₁

Assume f : α → β₁ ⊕ β₂ never reaches β₂ values. We convert f to α → β₁ function.

Equations

• fn_of_sum_ne_inr hf x✝ = ⋯.choose

theorem eq_of_fn_sum_ne_inl {β₁ β₂ α : Type} {f : α → β₁ ⊕ β₂} (hf : ∀ (a : α) (b₁ : β₁), f a ≠ ◩b₁) (i : α) : f i = ◪(fn_of_sum_ne_inl hf i)

theorem eq_of_fn_sum_ne_inr {β₁ β₂ α : Type} {f : α → β₁ ⊕ β₂} (hf : ∀ (a : α) (b₂ : β₂), f a ≠ ◪b₂) (i : α) : f i = ◩(fn_of_sum_ne_inr hf i)