Interaction between Sum.elim, ≤, and 0 or 1

This file provides basic API for part-wise comparison of Sum.elim vectors against 0 or 1.

theorem Sum.one_le_elim_iff {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [LE β] [One β] {v₁ : α₁ → β} {v₂ : α₂ → β} : 1 ≤ Sum.elim v₁ v₂ ↔ 1 ≤ v₁ ∧ 1 ≤ v₂

theorem Sum.nonneg_elim_iff {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [LE β] [Zero β] {v₁ : α₁ → β} {v₂ : α₂ → β} : 0 ≤ Sum.elim v₁ v₂ ↔ 0 ≤ v₁ ∧ 0 ≤ v₂

theorem Sum.elim_le_one_iff {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [LE β] [One β] {v₁ : α₁ → β} {v₂ : α₂ → β} : Sum.elim v₁ v₂ ≤ 1 ↔ v₁ ≤ 1 ∧ v₂ ≤ 1

theorem Sum.elim_nonpos_iff {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [LE β] [Zero β] {v₁ : α₁ → β} {v₂ : α₂ → β} : Sum.elim v₁ v₂ ≤ 0 ↔ v₁ ≤ 0 ∧ v₂ ≤ 0