elim_le_one_iff — Mathlib

English

Let β be ordered with a distinguished 1, and v1 : α1 → β, v2 : α2 → β. Then Sum.elim v1 v2 ≤ 1 if and only if v1 ≤ 1 and v2 ≤ 1 (pointwise).

Русский

Пусть β упорядочено, имеется единица 1. Пусть v1 : α1 → β и v2 : α2 → β. Тогда Sum.elim v1 v2 ≤ 1 тогда и только тогда, когда v1 ≤ 1 и v2 ≤ 1 (поэлементно).

LaTeX

$$$\mathrm{Sum}\,\mathrm{elim}(v_1,v_2) \le 1 \iff (v_1 \le 1) \land (v_2 \le 1)$$$

Lean4

@[to_additive]
theorem elim_le_one_iff : Sum.elim v₁ v₂ ≤ 1 ↔ v₁ ≤ 1 ∧ v₂ ≤ 1 :=
  elim_le_const_iff

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